removal of Main and other tidying up
authorpaulson
Mon Apr 11 16:25:31 2005 +0200 (2005-04-11)
changeset 15697681bcb7f0389
parent 15696 1da4ce092c0b
child 15698 95deeda57341
removal of Main and other tidying up
src/HOL/IsaMakefile
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_reconstruct_proof.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Apr 11 12:34:34 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Apr 11 16:25:31 2005 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4   Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
     1.5   Tools/res_axioms.ML Tools/res_types_sorts.ML \
     1.6   Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
     1.7 - Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \
     1.8 + Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \
     1.9   Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
    1.10   Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML   Tools/ATP/modUnix.ML  \
    1.11   Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
     2.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Mon Apr 11 12:34:34 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Mon Apr 11 16:25:31 2005 +0200
     2.3 @@ -3,8 +3,6 @@
     2.4  (*----------------------------------------------*)
     2.5  (* Reorder clauses for use in binary resolution *)
     2.6  (*----------------------------------------------*)
     2.7 -fun take n [] = []
     2.8 -|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
     2.9  
    2.10  fun drop n [] = []
    2.11  |   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
    2.12 @@ -13,7 +11,7 @@
    2.13  |   remove n (x::xs) = List.filter (not_equal n) (x::xs);
    2.14  
    2.15  fun remove_nth n [] = []
    2.16 -|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
    2.17 +|   remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
    2.18  
    2.19  fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
    2.20  
    2.21 @@ -28,21 +26,6 @@
    2.22       
    2.23  exception Not_in_list;  
    2.24  
    2.25 -
    2.26 -
    2.27 -
    2.28 -   (* get the literals from a disjunctive clause *)
    2.29 -
    2.30 -(*fun get_disj_literals t = if is_disj t then
    2.31 -			           let 
    2.32 -                                      val {disj1, disj2} = dest_disj t  
    2.33 -                                   in 
    2.34 -                                      disj1::(get_disj_literals disj2)
    2.35 -                                   end
    2.36 -                                else
    2.37 -                                    ([t])
    2.38 -   
    2.39 -*)
    2.40               
    2.41  (*
    2.42  (* gives horn clause with kth disj as concl (starting at 1) *)
    2.43 @@ -99,22 +82,6 @@
    2.44  exception Not_in_list;  
    2.45  
    2.46  
    2.47 -(*Permute a rule's premises to move the i-th premise to the last position.*)
    2.48 -fun make_last i th =
    2.49 -  let val n = nprems_of th 
    2.50 -  in  if 1 <= i andalso i <= n 
    2.51 -      then Thm.permute_prems (i-1) 1 th
    2.52 -      else raise THM("make_last", i, [th])
    2.53 -  end;
    2.54 -
    2.55 -(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
    2.56 -  double-negations.*)
    2.57 -val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
    2.58 -
    2.59 -(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
    2.60 -fun select_literal i cl = negate_head (make_last i cl);
    2.61 -
    2.62 -
    2.63  (* get a meta-clause for resolution with correct order of literals *)
    2.64  fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
    2.65                                val contra =  if lits = 1 
    2.66 @@ -133,10 +100,6 @@
    2.67  
    2.68  
    2.69  
    2.70 -
    2.71 -
    2.72 -
    2.73 -
    2.74  fun zip xs [] = []
    2.75  |   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
    2.76  
    2.77 @@ -381,14 +344,6 @@
    2.78                                  *)
    2.79  
    2.80  
    2.81 -
    2.82 -
    2.83 -
    2.84 -
    2.85 -
    2.86 -
    2.87 -
    2.88 -
    2.89  (* checkorder Spass Isabelle [] *)
    2.90  
    2.91  fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
     3.1 --- a/src/HOL/Tools/ATP/recon_reconstruct_proof.ML	Mon Apr 11 12:34:34 2005 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,308 +0,0 @@
     3.4 -
     3.5 -
     3.6 -(****************************************)
     3.7 -(* Reconstruct an axiom resolution step *)
     3.8 -(****************************************)
     3.9 -
    3.10 - fun reconstruct_axiom clauses (clausenum:int) thml (numlist, symlist, nsymlist ) =  
    3.11 -                                     let val this_axiom =(assoc  clausenum clauses)
    3.12 -                                         val symmed = (apply_rule sym  symlist this_axiom)
    3.13 -                                         val nsymmed = (apply_rule not_sym nsymlist  symmed )
    3.14 -                                     in
    3.15 -                                         rearrange_prems numlist nsymmed
    3.16 -                                     end
    3.17 -
    3.18 -(****************************************)
    3.19 -(* Reconstruct a binary resolution step *)
    3.20 -(****************************************)
    3.21 -
    3.22 -fun reconstruct_binary ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )
    3.23 -        = let
    3.24 -              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
    3.25 -              val thm2 =  assoc  clause2 thml
    3.26 -              val res =   thm1 RSN ((lit2 +1), thm2)
    3.27 -              val symmed = (apply_rule sym  symlist res)
    3.28 -              val nsymmed = (apply_rule not_sym nsymlist  symmed )
    3.29 -          in
    3.30 -              rearrange_prems numlist nsymmed
    3.31 -          end
    3.32 -
    3.33 -
    3.34 -(****************************************)
    3.35 -(* Reconstruct a binary resolution step *)
    3.36 -(****************************************)
    3.37 -
    3.38 -fun reconstruct_mrr ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )
    3.39 -        = let
    3.40 -              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
    3.41 -              val thm2 =  assoc  clause2 thml
    3.42 -              val res =   thm1 RSN ((lit2 +1), thm2)
    3.43 -              val symmed = (apply_rule sym  symlist res)
    3.44 -              val nsymmed = (apply_rule not_sym nsymlist  symmed )
    3.45 -          in
    3.46 -              rearrange_prems numlist nsymmed
    3.47 -          end
    3.48 -
    3.49 -(*******************************************)
    3.50 -(* Reconstruct a factoring resolution step *)
    3.51 -(*******************************************)
    3.52 -
    3.53 -fun reconstruct_factor (clause,  lit1, lit2) thml (numlist, symlist, nsymlist )= 
    3.54 -                          let 
    3.55 -                            val th =  assoc clause thml
    3.56 -                            val prems = prems_of th
    3.57 -                            val fac1 = get_nth (lit1+1) prems
    3.58 -                            val fac2 = get_nth (lit2+1) prems
    3.59 -                            val unif_env = unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
    3.60 -                            val newenv = getnewenv unif_env
    3.61 -                            val envlist = alist_of newenv
    3.62 -                            
    3.63 -                            val newsubsts = mksubstlist envlist []
    3.64 -                          in 
    3.65 -                            if (is_Var (fst(hd(newsubsts))))
    3.66 -                            then
    3.67 -                                let 
    3.68 -                                   val str1 = lit_string_with_nums (fst (hd newsubsts));
    3.69 -                                   val str2 = lit_string_with_nums (snd (hd newsubsts));
    3.70 -                                   val facthm = read_instantiate [(str1,str2)] th;
    3.71 -                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    3.72 -                                   val symmed = (apply_rule sym  symlist res)
    3.73 -                                   val nsymmed = (apply_rule not_sym nsymlist  symmed )
    3.74 -         
    3.75 -                                in 
    3.76 -                                   rearrange_prems numlist nsymmed
    3.77 -                                end
    3.78 -                            else
    3.79 -                                let
    3.80 -                                   val str2 = lit_string_with_nums (fst (hd newsubsts));
    3.81 -                                   val str1 = lit_string_with_nums (snd (hd newsubsts));
    3.82 -                                   val facthm = read_instantiate [(str1,str2)] th;
    3.83 -                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    3.84 -                                   val symmed = (apply_rule sym  symlist res)
    3.85 -                                   val nsymmed = (apply_rule not_sym nsymlist  symmed )
    3.86 -                                in 
    3.87 -                                    rearrange_prems numlist nsymmed    
    3.88 -                                end
    3.89 -                         end;
    3.90 -
    3.91 -
    3.92 -(****************************************)
    3.93 -(* Reconstruct a paramodulation step    *)
    3.94 -(****************************************)
    3.95 -
    3.96 -                          (* clause1, lit1 is thing to rewrite with *)
    3.97 -fun reconstruct_standard_para_left ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )= 
    3.98 -
    3.99 -                          let 
   3.100 -                             
   3.101 -                              val newthm = para_left ((clause1, lit1), (clause2 , lit2))  thml 
   3.102 -                              val symmed = (apply_rule sym  symlist newthm)
   3.103 -                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   3.104 -                                
   3.105 -                         in
   3.106 -                              rearrange_prems numlist nsymmed  
   3.107 -                         end
   3.108 -
   3.109 -
   3.110 -
   3.111 -                        (* clause1, lit1 is thing to rewrite with *)
   3.112 -fun reconstruct_standard_para_right ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )= 
   3.113 -
   3.114 -                          let 
   3.115 -                             
   3.116 -                              val newthm = para_right ((clause1, lit1), (clause2 , lit2))  thml 
   3.117 -                              val symmed = (apply_rule sym  symlist newthm)
   3.118 -                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   3.119 -                                
   3.120 -                         in
   3.121 -                              rearrange_prems numlist nsymmed  
   3.122 -                         end
   3.123 -
   3.124 -
   3.125 -
   3.126 -
   3.127 -
   3.128 -
   3.129 -
   3.130 -
   3.131 -                        (*  let 
   3.132 -                            val th1 =  assoc clause1 thml
   3.133 -                            val th2 =  assoc clause2 thml 
   3.134 -                            val prems1 = prems_of th1
   3.135 -                            val prems2 = prems_of th2
   3.136 -                            (* want to get first element of equality *)
   3.137 -
   3.138 -                            val fac1 = get_nth (lit1+1) prems1
   3.139 -                            val {lhs, rhs} = dest_eq(dest_Trueprop fac1)
   3.140 -                                             handle ERR _ => dest_eq(dest_neg (dest_Trueprop fac1))
   3.141 -                            (* get other literal involved in the paramodulation *)
   3.142 -                            val fac2 = get_nth (lit2+1) prems2
   3.143 -
   3.144 -                           (* get bit of th2 to unify with lhs of th1 *)
   3.145 -                            val unif_lit = get_unif_lit (dest_Trueprop fac2) lhs
   3.146 -                            val unif_env = unifiers (Mainsign,Envir.empty 0, [(unif_lit, lhs)])
   3.147 -                            val newenv = getnewenv unif_env
   3.148 -                            val envlist = alist_of newenv
   3.149 -                            val newsubsts = mksubstlist envlist []
   3.150 -                           (* instantiate th2 with unifiers *)
   3.151 -                          
   3.152 -                            val newth1 =  
   3.153 -                              if (is_Var (fst(hd(newsubsts))))
   3.154 -                              then
   3.155 -                                  let 
   3.156 -                                     val str1 = lit_string_with_nums (fst (hd newsubsts));
   3.157 -                                     val str2 = lit_string_with_nums (snd (hd newsubsts));
   3.158 -                                     val facthm = read_instantiate [(str1,str2)] th1
   3.159 -                                  in 
   3.160 -                                     hd (Seq.list_of(distinct_subgoals_tac facthm))
   3.161 -                                  end
   3.162 -                              else
   3.163 -                                  let
   3.164 -                                     val str2 = lit_string_with_nums (fst (hd newsubsts));
   3.165 -                                     val str1 = lit_string_with_nums  (snd (hd newsubsts));
   3.166 -                                     val facthm = read_instantiate [(str1,str2)] th1
   3.167 -                                  in 
   3.168 -                                     hd (Seq.list_of(distinct_subgoals_tac facthm))
   3.169 -                                  end
   3.170 -                           (*rewrite th2 with the equality bit of th2 i.e. lit2 *)
   3.171 -                              val facthm' = select_literal  (lit1 + 1) newth1
   3.172 -                              val equal_lit = concl_of facthm'
   3.173 -                              val cterm_eq = cterm_of Mainsign equal_lit  
   3.174 -                              val eq_thm = assume cterm_eq
   3.175 -                              val meta_eq_thm = mk_meta_eq eq_thm
   3.176 -                              val newth2= rewrite_rule [meta_eq_thm] th2
   3.177 -                           (*thin lit2 from th2 *)
   3.178 -                           (* get th1 with lit one as concl, then resolve with thin_rl *)
   3.179 -                              val thm' = facthm' RS thin_rl
   3.180 -                           (* now resolve th2 with last premise of thm' *)
   3.181 -                              val newthm = newth2  RSN ((length prems1), thm')
   3.182 -                              val symmed = (apply_rule sym  symlist newthm)
   3.183 -                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   3.184 -                                
   3.185 -                         in
   3.186 -                              rearrange_prems numlist nsymmed  
   3.187 -                         end
   3.188 -
   3.189 -*)
   3.190 -
   3.191 -
   3.192 -(********************************************)
   3.193 -(* Reconstruct a rewrite step               *)
   3.194 -(********************************************)
   3.195 -
   3.196 -
   3.197 -
   3.198 -
   3.199 -
   3.200 -
   3.201 -(* does rewriting involve every literal in rewritten clause? *)
   3.202 -                    (* clause1, lit1 is thing to rewrite with *)
   3.203 -
   3.204 -fun reconstruct_rewrite (clause1, lit1, clause2) thml  (numlist, symlist, nsymlist )=
   3.205 -
   3.206 -                          let val th1 =  assoc clause1 thml
   3.207 -                              val th2 =  assoc clause2 thml 
   3.208 -                              val eq_lit_th = select_literal (lit1+1) th1
   3.209 -                              val equal_lit = concl_of eq_lit_th
   3.210 -                              val cterm_eq = cterm_of Mainsign  equal_lit 
   3.211 -                              val eq_thm = assume cterm_eq
   3.212 -                              val meta_eq_thm = mk_meta_eq eq_thm
   3.213 -                              val newth2= rewrite_rule [meta_eq_thm] th2
   3.214 -                             val symmed = (apply_rule sym  symlist newth2)
   3.215 -                              val nsymmed = (apply_rule not_sym nsymlist  symmed )
   3.216 -                                
   3.217 -                           in
   3.218 -                              rearrange_prems numlist nsymmed  
   3.219 -                           end
   3.220 -
   3.221 -
   3.222 -
   3.223 -(*****************************************)
   3.224 -(* Reconstruct an obvious reduction step *)
   3.225 -(*****************************************)
   3.226 -
   3.227 -
   3.228 -fun reconstruct_obvious  (clause1, lit1)  allvars thml clause_strs= 
   3.229 -                           let val th1 =  assoc clause1 thml
   3.230 -                               val prems1 = prems_of th1
   3.231 -                               val newthm = refl RSN ((lit1+ 1), th1)
   3.232 -                                               handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
   3.233 -                               val symmed = (apply_rule sym  symlist newthm)
   3.234 -                               val nsymmed = (apply_rule not_sym nsymlist  symmed )
   3.235 -                           in 
   3.236 -                               rearrange_prems numlist nsymmed  
   3.237 -                           end
   3.238 -
   3.239 -
   3.240 -
   3.241 -(********************************************************************************************)
   3.242 -(* reconstruct a single step of the res. proof - depending on what sort of proof step it was*)
   3.243 -(********************************************************************************************)
   3.244 -
   3.245 -
   3.246 - fun reconstruct_proof clauses clausenum thml  Axiom (numlist, symlist, nsymlist)
   3.247 -        = reconstruct_axiom clauses clausenum thml  (numlist, symlist, nsymlist)
   3.248 -      | reconstruct_proof clauses clausenum  thml (Binary (a, b)) (numlist, symlist, nsymlist)
   3.249 -        = reconstruct_binary (a, b) thml (numlist, symlist, nsymlist)
   3.250 -       | reconstruct_proof clauses clausenum  thml (MRR (a, b)) (numlist, symlist, nsymlist)
   3.251 -        = reconstruct_mrr (a, b) thml (numlist, symlist, nsymlist)
   3.252 -      | reconstruct_proof clauses clausenum  thml (Factor (a, b, c)) (numlist, symlist, nsymlist)
   3.253 -         = reconstruct_factor (a ,b ,c) thml (numlist, symlist, nsymlist)
   3.254 -      | reconstruct_proof clauses clausenum  thml (Para (a, b)) (numlist, symlist, nsymlist)
   3.255 -        = reconstruct_standard_para (a, b) thml (numlist, symlist, nsymlist)
   3.256 -      | reconstruct_proof clauses clausenum thml (Rewrite (a,b,c)) (numlist, symlist, nsymlist)
   3.257 -        = reconstruct_rewrite (a,b,c) thml (numlist, symlist, nsymlist)
   3.258 -      | reconstruct_proof clauses clausenum thml (Obvious (a,b)) (numlist, symlist, nsymlist)
   3.259 -        = reconstruct_obvious (a,b) thml (numlist, symlist, nsymlist)
   3.260 -      (*| reconstruct_proof clauses  clausenum thml (Hyper l)
   3.261 -        = reconstruct_hyper l thml*)
   3.262 -      | reconstruct_proof clauses clausenum  thml _ _ =
   3.263 -          raise ASSERTION  "proof step not implemented"
   3.264 -
   3.265 -
   3.266 -(********************************************************************************************)
   3.267 -(* reconstruct a single line of the res. proof - at the moment do only inference steps      *)
   3.268 -(********************************************************************************************)
   3.269 -
   3.270 -    fun reconstruct_line clauses thml (clause_num, (proof_step, numlist, symlist,nsymlist))
   3.271 -        = let
   3.272 -            val thm = reconstruct_proof clauses clause_num thml proof_step (numlist, symlist,nsymlist)
   3.273 -            
   3.274 -          in
   3.275 -            (clause_num, thm)::thml
   3.276 -          end
   3.277 -
   3.278 -(********************************************************************)
   3.279 -(* reconstruct through the res. proof, creating an Isabelle theorem *)
   3.280 -(********************************************************************)
   3.281 -
   3.282 -
   3.283 -fun reconstruct clauses [] thml  = ((snd( hd thml)))
   3.284 -      | reconstruct clauses (h::t) thml  
   3.285 -        = let
   3.286 -            val (thml') = reconstruct_line clauses thml h 
   3.287 -            val  (thm) = reconstruct clauses t thml' 
   3.288 -          in
   3.289 -             (thm)
   3.290 -          end
   3.291 -
   3.292 -
   3.293 -(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
   3.294 - (* and the proof as a list of the proper datatype *)
   3.295 -(* take the cnf clauses of the goal and the proof from the res. prover *)
   3.296 -(* as a list of type Proofstep and return the thm goal ==> False *)
   3.297 -
   3.298 -fun first_pair (a,b,c) = (a,b);
   3.299 -
   3.300 -fun second_pair (a,b,c) = (b,c);
   3.301 -
   3.302 -(*************************)
   3.303 -(* reconstruct res proof *)
   3.304 -(*************************)
   3.305 -
   3.306 -fun reconstruct_proof clauses proof
   3.307 -        = let val thm = reconstruct clauses proof [] 
   3.308 -          in
   3.309 -             thm
   3.310 -          end
   3.311 -  
     4.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Apr 11 12:34:34 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Apr 11 16:25:31 2005 +0200
     4.3 @@ -15,7 +15,7 @@
     4.4  (* Versions that include type information *)
     4.5   
     4.6  fun string_of_thm thm = let val _ = set show_sorts
     4.7 -                                val str = Sign.string_of_term Mainsign (prop_of thm)
     4.8 +                                val str = string_of_thm thm
     4.9                                  val no_returns =List.filter not_newline (explode str)
    4.10                                  val _ = reset show_sorts
    4.11                              in 
    4.12 @@ -149,28 +149,6 @@
    4.13                                        add_if_not_inlist ys xs (y::newlist)
    4.14                                          else add_if_not_inlist ys xs (newlist)
    4.15  
    4.16 -(*
    4.17 -fun is_alpha_space_neg_eq_colon ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse  ( ch = ";") orelse( ch = "=")
    4.18 -
    4.19 -(* replace | by ; here *)
    4.20 -fun change_or [] = []
    4.21 -|   change_or (x::xs) = if x = "|" 
    4.22 -                          then 
    4.23 -                             [";"]@(change_or xs)
    4.24 -                          else (x::(change_or xs))
    4.25 -
    4.26 -
    4.27 -fun clause_lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
    4.28 -                              val exp_term = explode termstr
    4.29 -                              val colon_term = change_or exp_term
    4.30 -                   in
    4.31 -                             implode(List.filter is_alpha_space_neg_eq_colon colon_term)
    4.32 -                   end
    4.33 -
    4.34 -fun get_clause_lits thm =  clause_lit_string (prop_of thm)
    4.35 -*)
    4.36 -
    4.37 -
    4.38  fun onestr [] str = str
    4.39  |   onestr (x::xs) str = onestr xs (str^(concat x))
    4.40  
    4.41 @@ -181,83 +159,10 @@
    4.42  |   onelist (x::xs) newlist = onelist xs (newlist@x)
    4.43  
    4.44  
    4.45 -(**** Code to support ordinary resolution, rather than Model Elimination ****)
    4.46 -
    4.47 -(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), 
    4.48 -  with no contrapositives, for ordinary resolution.*)
    4.49 -
    4.50 -(*raises exception if no rules apply -- unlike RL*)
    4.51 -fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
    4.52 -  | tryres (th, []) = raise THM("tryres", 0, [th]);
    4.53  
    4.54  val prop_of = #prop o rep_thm;
    4.55  
    4.56  
    4.57 -(*For ordinary resolution. *)
    4.58 -val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule'];
    4.59 -(*Use "theorem naming" to label the clauses*)
    4.60 -fun name_thms label =
    4.61 -    let fun name1 (th, (k,ths)) =
    4.62 -	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
    4.63 -
    4.64 -    in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    4.65 -
    4.66 -(*Find an all-negative support clause*)
    4.67 -fun is_negative th = forall (not o #1) (literals (prop_of th));
    4.68 -
    4.69 -val neg_clauses = List.filter is_negative;
    4.70 -
    4.71 -
    4.72 -
    4.73 -(*True if the given type contains bool anywhere*)
    4.74 -fun has_bool (Type("bool",_)) = true
    4.75 -  | has_bool (Type(_, Ts)) = exists has_bool Ts
    4.76 -  | has_bool _ = false;
    4.77 -  
    4.78 -
    4.79 -(*Create a meta-level Horn clause*)
    4.80 -fun make_horn crules th = make_horn crules (tryres(th,crules))
    4.81 -			  handle THM _ => th;
    4.82 -
    4.83 -
    4.84 -(*Raises an exception if any Vars in the theorem mention type bool. That would mean
    4.85 -  they are higher-order, and in addition, they could cause make_horn to loop!*)
    4.86 -fun check_no_bool th =
    4.87 -  if exists (has_bool o fastype_of) (term_vars (#prop (rep_thm th)))
    4.88 -  then raise THM ("check_no_bool", 0, [th]) else th;
    4.89 -
    4.90 -
    4.91 -(*Rules to convert the head literal into a negated assumption. If the head
    4.92 -  literal is already negated, then using notEfalse instead of notEfalse'
    4.93 -  prevents a double negation.*)
    4.94 -val notEfalse = read_instantiate [("R","False")] notE;
    4.95 -val notEfalse' = rotate_prems 1 notEfalse;
    4.96 -
    4.97 -fun negated_asm_of_head th = 
    4.98 -    th RS notEfalse handle THM _ => th RS notEfalse';
    4.99 -
   4.100 -(*Converting one clause*)
   4.101 -fun make_meta_clause th = 
   4.102 -	negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th));
   4.103 -
   4.104 -fun make_meta_clauses ths =
   4.105 -    name_thms "MClause#"
   4.106 -      (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
   4.107 -
   4.108 -(*Permute a rule's premises to move the i-th premise to the last position.*)
   4.109 -fun make_last i th =
   4.110 -  let val n = nprems_of th 
   4.111 -  in  if 1 <= i andalso i <= n 
   4.112 -      then Thm.permute_prems (i-1) 1 th
   4.113 -      else raise THM("select_literal", i, [th])
   4.114 -  end;
   4.115 -
   4.116 -(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   4.117 -  double-negations.*)
   4.118 -val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   4.119 -
   4.120 -(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   4.121 -fun select_literal i cl = negate_head (make_last i cl);
   4.122  
   4.123   fun get_axioms_used proof_steps thmstring = let 
   4.124                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
   4.125 @@ -281,7 +186,7 @@
   4.126  
   4.127                                              val distfrees = distinct frees
   4.128  
   4.129 -                                            val metas = map make_meta_clause clauses
   4.130 +                                            val metas = map Meson.make_meta_clause clauses
   4.131                                              val ax_strs = map #3 axioms
   4.132  
   4.133                                              (* literals of -all- axioms, not just those used by spass *)
     5.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Mon Apr 11 12:34:34 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Mon Apr 11 16:25:31 2005 +0200
     5.3 @@ -1,17 +1,4 @@
     5.4  
     5.5 -fun take n [] = []
     5.6 -|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
     5.7 -
     5.8 -fun drop n [] = []
     5.9 -|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
    5.10 -
    5.11 -fun remove n [] = []
    5.12 -|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
    5.13 -
    5.14 -fun remove_nth n [] = []
    5.15 -|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
    5.16 -
    5.17 -fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
    5.18  
    5.19  fun add_in_order (x:string) [] = [x]
    5.20  |   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
    5.21 @@ -69,7 +56,7 @@
    5.22  
    5.23  
    5.24  
    5.25 -fun lit_string_with_nums t = let val termstr = (Sign.string_of_term Mainsign) t
    5.26 +fun lit_string_with_nums t = let val termstr = Term.string_of_term t
    5.27                                   val exp_term = explode termstr
    5.28                               in
    5.29                                   implode(List.filter is_alpha_space_digit_or_neg exp_term)
    5.30 @@ -158,19 +145,20 @@
    5.31                            let 
    5.32                              val th =  Recon_Base.assoc clause thml
    5.33                              val prems = prems_of th
    5.34 +                            val sign = sign_of_thm th
    5.35                              val fac1 = get_nth (lit1+1) prems
    5.36                              val fac2 = get_nth (lit2+1) prems
    5.37                              val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
    5.38                              val newenv = getnewenv unif_env
    5.39                              val envlist = Envir.alist_of newenv
    5.40                              
    5.41 -                            val newsubsts = mksubstlist envlist []
    5.42 +                            val (t1,t2)::_ = mksubstlist envlist []
    5.43                            in 
    5.44 -                            if (is_Var (fst(hd(newsubsts))))
    5.45 +                            if (is_Var t1)
    5.46                              then
    5.47                                  let 
    5.48 -                                   val str1 = lit_string_with_nums (fst (hd newsubsts));
    5.49 -                                   val str2 = lit_string_with_nums (snd (hd newsubsts));
    5.50 +                                   val str1 = lit_string_with_nums t1;
    5.51 +                                   val str2 = lit_string_with_nums t2;
    5.52                                     val facthm = read_instantiate [(str1,str2)] th;
    5.53                                     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    5.54                                     val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    5.55 @@ -180,8 +168,8 @@
    5.56                                  end
    5.57                              else
    5.58                                  let
    5.59 -                                   val str2 = lit_string_with_nums (fst (hd newsubsts));
    5.60 -                                   val str1 = lit_string_with_nums (snd (hd newsubsts));
    5.61 +                                   val str2 = lit_string_with_nums t1;
    5.62 +                                   val str1 = lit_string_with_nums t2;
    5.63                                     val facthm = read_instantiate [(str1,str2)] th;
    5.64                                     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
    5.65                                     val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    5.66 @@ -282,7 +270,7 @@
    5.67            val eqsubst = eq_lit_th RSN (2,rev_subst)
    5.68            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
    5.69  eqsubst)
    5.70 -     in negated_asm_of_head newth end;
    5.71 +     in Meson.negated_asm_of_head newth end;
    5.72  
    5.73  val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
    5.74  eqsubst)
     6.1 --- a/src/HOL/Tools/res_atp.ML	Mon Apr 11 12:34:34 2005 +0200
     6.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Apr 11 16:25:31 2005 +0200
     6.3 @@ -146,13 +146,13 @@
     6.4  (* should be modified to allow other provers to be called            *)
     6.5  (*********************************************************************)
     6.6  
     6.7 -fun call_resolve_tac thms sg_term (childin, childout,pid) n  = let
     6.8 +fun call_resolve_tac sign thms sg_term (childin, childout,pid) n  = let
     6.9                               val thmstring = concat_with_and (map string_of_thm thms) ""
    6.10                               val thm_no = length thms
    6.11                               val _ = warning ("number of thms is : "^(string_of_int thm_no))
    6.12                               val _ = warning ("thmstring in call_res is: "^thmstring)
    6.13  
    6.14 -                             val goalstr = Sign.string_of_term Mainsign sg_term 
    6.15 +                             val goalstr = Sign.string_of_term sign sg_term 
    6.16                               val goalproofstring = proofstring goalstr
    6.17                               val no_returns =List.filter not_newline ( goalproofstring)
    6.18                               val goalstring = implode no_returns
    6.19 @@ -165,7 +165,7 @@
    6.20                               (*val _ = tptp_inputs clauses prob_file*)
    6.21                               val thmstring = concat_with_and (map string_of_thm thms) ""
    6.22                             
    6.23 -                             val goalstr = Sign.string_of_term Mainsign sg_term 
    6.24 +                             val goalstr = Sign.string_of_term sign sg_term 
    6.25                               val goalproofstring = proofstring goalstr
    6.26                               val no_returns =List.filter not_newline ( goalproofstring)
    6.27                               val goalstring = implode no_returns
    6.28 @@ -226,36 +226,25 @@
    6.29  
    6.30  (* dummy tac vs.  Doesn't call resolve_tac *)
    6.31  
    6.32 -fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = 
    6.33 -                                         ( (warning("ths for tptp: "^(concat_with_and (map string_of_thm thms) "")));
    6.34 -                                           (warning("in call_atp_tac_tfrees"));
    6.35 +fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
    6.36 +                                         ( warning("ths for tptp: " ^ (concat_with_and (map string_of_thm thms) ""));
    6.37 +                                           warning("in call_atp_tac_tfrees");
    6.38                                             
    6.39                                             tptp_inputs_tfrees (make_clauses thms) n tfrees;
    6.40 -                                           call_resolve_tac thms sg_term (childin, childout, pid) n;
    6.41 +                                           call_resolve_tac sign thms sg_term (childin, childout, pid) n;
    6.42    					   dummy_tac);
    6.43  
    6.44 -
    6.45 -(*
    6.46 -fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
    6.47 -let val _ = (warning ("in atp_tac_tfrees "))
    6.48 -   in
    6.49 -SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac,*) METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) "")));(*make_clauses negs;*)dummy_tac)) ])1
    6.50 -end;
    6.51 -
    6.52 -
    6.53 -
    6.54 -METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) ""))));make_clauses negs;dummy_tac)) 1;
    6.55 -*)
    6.56 -
    6.57 -
    6.58 -fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n  = 
    6.59 -let val _ = (warning ("in atp_tac_tfrees "))
    6.60 -    val _ = (warning ("sg_term :"^((Sign.string_of_term Mainsign) sg_term)))
    6.61 +fun atp_tac_tfrees tfrees sg_term (childin, childout,pid)  n st = 
    6.62 +let val sign = sign_of_thm st
    6.63 +    val _ = warning ("in atp_tac_tfrees ")
    6.64 +    val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term))
    6.65     
    6.66     in
    6.67  SELECT_GOAL
    6.68    (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    6.69 -  METAHYPS(fn negs => ((warning("calling  call_atp_tac_tfrees with negs"^(concat_with_and (map  string_of_thm negs) "")));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n
    6.70 +  METAHYPS(fn negs => (warning("calling  call_atp_tac_tfrees with negs"
    6.71 +                               ^ (concat_with_and (map string_of_thm negs) ""));
    6.72 +           call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
    6.73  end;
    6.74  
    6.75  
    6.76 @@ -315,9 +304,10 @@
    6.77      let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    6.78          val _= (warning ("in isar_atp'"))
    6.79          val prems = prems_of thm
    6.80 +        val sign = sign_of_thm thm
    6.81          val thms_string =concat_with_and (map  string_of_thm thms) ""
    6.82          val thmstring = string_of_thm thm
    6.83 -        val prems_string = concat_with_and (map (Sign.string_of_term Mainsign) prems) ""
    6.84 +        val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
    6.85          (* set up variables for writing out the clasimps to a tptp file *)
    6.86          (* val _ = write_out_clasimp (File.sysify_path axiom_file)*)
    6.87          (* cq: add write out clasimps to file *)
    6.88 @@ -405,8 +395,9 @@
    6.89          val d_ss_thms = Simplifier.get_delta_simpset ctxt
    6.90          val thmstring = string_of_thm thm
    6.91          val sg_prems = prems_of thm
    6.92 +        val sign = sign_of_thm thm
    6.93          val prem_no = length sg_prems
    6.94 -        val prems_string =  concat_with_and (map (Sign.string_of_term Mainsign) sg_prems) ""
    6.95 +        val prems_string =  concat_with_and (map (Sign.string_of_term sign) sg_prems) ""
    6.96      in
    6.97           
    6.98            (warning ("initial thm in isar_atp: "^thmstring));