src/HOL/Tools/ATP/recon_order_clauses.ML
changeset 15697 681bcb7f0389
parent 15684 5ec4d21889d6
child 15700 970e0293dfb3
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Mon Apr 11 12:34:34 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Mon Apr 11 16:25:31 2005 +0200
     1.3 @@ -3,8 +3,6 @@
     1.4  (*----------------------------------------------*)
     1.5  (* Reorder clauses for use in binary resolution *)
     1.6  (*----------------------------------------------*)
     1.7 -fun take n [] = []
     1.8 -|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
     1.9  
    1.10  fun drop n [] = []
    1.11  |   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
    1.12 @@ -13,7 +11,7 @@
    1.13  |   remove n (x::xs) = List.filter (not_equal n) (x::xs);
    1.14  
    1.15  fun remove_nth n [] = []
    1.16 -|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
    1.17 +|   remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
    1.18  
    1.19  fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
    1.20  
    1.21 @@ -28,21 +26,6 @@
    1.22       
    1.23  exception Not_in_list;  
    1.24  
    1.25 -
    1.26 -
    1.27 -
    1.28 -   (* get the literals from a disjunctive clause *)
    1.29 -
    1.30 -(*fun get_disj_literals t = if is_disj t then
    1.31 -			           let 
    1.32 -                                      val {disj1, disj2} = dest_disj t  
    1.33 -                                   in 
    1.34 -                                      disj1::(get_disj_literals disj2)
    1.35 -                                   end
    1.36 -                                else
    1.37 -                                    ([t])
    1.38 -   
    1.39 -*)
    1.40               
    1.41  (*
    1.42  (* gives horn clause with kth disj as concl (starting at 1) *)
    1.43 @@ -99,22 +82,6 @@
    1.44  exception Not_in_list;  
    1.45  
    1.46  
    1.47 -(*Permute a rule's premises to move the i-th premise to the last position.*)
    1.48 -fun make_last i th =
    1.49 -  let val n = nprems_of th 
    1.50 -  in  if 1 <= i andalso i <= n 
    1.51 -      then Thm.permute_prems (i-1) 1 th
    1.52 -      else raise THM("make_last", i, [th])
    1.53 -  end;
    1.54 -
    1.55 -(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
    1.56 -  double-negations.*)
    1.57 -val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
    1.58 -
    1.59 -(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
    1.60 -fun select_literal i cl = negate_head (make_last i cl);
    1.61 -
    1.62 -
    1.63  (* get a meta-clause for resolution with correct order of literals *)
    1.64  fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
    1.65                                val contra =  if lits = 1 
    1.66 @@ -133,10 +100,6 @@
    1.67  
    1.68  
    1.69  
    1.70 -
    1.71 -
    1.72 -
    1.73 -
    1.74  fun zip xs [] = []
    1.75  |   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
    1.76  
    1.77 @@ -381,14 +344,6 @@
    1.78                                  *)
    1.79  
    1.80  
    1.81 -
    1.82 -
    1.83 -
    1.84 -
    1.85 -
    1.86 -
    1.87 -
    1.88 -
    1.89  (* checkorder Spass Isabelle [] *)
    1.90  
    1.91  fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)