src/HOL/Tools/ATP/recon_order_clauses.ML
changeset 15700 970e0293dfb3
parent 15697 681bcb7f0389
child 15702 2677db44c795
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 12 11:07:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 12 11:08:25 2005 +0200
     1.3 @@ -16,139 +16,8 @@
     1.4  fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
     1.5  
     1.6  
     1.7 - fun literals (Const("Trueprop",_) $ P) = literals P
     1.8 -   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
     1.9 -   | literals (Const("Not",_) $ P) = [(false,P)]
    1.10 -   | literals P = [(true,P)];
    1.11 -
    1.12 - (*number of literals in a term*)
    1.13 - val nliterals = length o literals; 
    1.14 -     
    1.15  exception Not_in_list;  
    1.16  
    1.17 -             
    1.18 -(*
    1.19 -(* gives horn clause with kth disj as concl (starting at 1) *)
    1.20 -fun rots (0,th) =  (Meson.make_horn Meson.crules th)
    1.21 -         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
    1.22 -
    1.23 -
    1.24 -                
    1.25 -Goal " (~~P) == P";
    1.26 -by Auto_tac;
    1.27 -qed "notnotEq";
    1.28 -
    1.29 -Goal "A | A ==> A";
    1.30 -by Auto_tac;
    1.31 -qed "rem_dup_disj";
    1.32 -
    1.33 -
    1.34 -
    1.35 -
    1.36 -(* New Meson code  Versions of make_neg_rule and make_pos_rule that don't insert new *)
    1.37 -(* assumptions, for ordinary resolution. *)
    1.38 -
    1.39 -
    1.40 -
    1.41 -
    1.42 - val not_conjD = thm "meson_not_conjD";
    1.43 - val not_disjD = thm "meson_not_disjD";
    1.44 - val not_notD = thm "meson_not_notD";
    1.45 - val not_allD = thm "meson_not_allD";
    1.46 - val not_exD = thm "meson_not_exD";
    1.47 - val imp_to_disjD = thm "meson_imp_to_disjD";
    1.48 - val not_impD = thm "meson_not_impD";
    1.49 - val iff_to_disjD = thm "meson_iff_to_disjD";
    1.50 - val not_iffD = thm "meson_not_iffD";
    1.51 - val conj_exD1 = thm "meson_conj_exD1";
    1.52 - val conj_exD2 = thm "meson_conj_exD2";
    1.53 - val disj_exD = thm "meson_disj_exD";
    1.54 - val disj_exD1 = thm "meson_disj_exD1";
    1.55 - val disj_exD2 = thm "meson_disj_exD2";
    1.56 - val disj_assoc = thm "meson_disj_assoc";
    1.57 - val disj_comm = thm "meson_disj_comm";
    1.58 - val disj_FalseD1 = thm "meson_disj_FalseD1";
    1.59 - val disj_FalseD2 = thm "meson_disj_FalseD2";
    1.60 -
    1.61 -
    1.62 - fun literals (Const("Trueprop",_) $ P) = literals P
    1.63 -   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
    1.64 -   | literals (Const("Not",_) $ P) = [(false,P)]
    1.65 -   | literals P = [(true,P)];
    1.66 -
    1.67 - (*number of literals in a term*)
    1.68 - val nliterals = length o literals; 
    1.69 -     
    1.70 -exception Not_in_list;  
    1.71 -
    1.72 -
    1.73 -(* get a meta-clause for resolution with correct order of literals *)
    1.74 -fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
    1.75 -                              val contra =  if lits = 1 
    1.76 -                                                 then
    1.77 -                                                     th
    1.78 -                                                 else
    1.79 -                                                     rots (n,th)   
    1.80 -                          in 
    1.81 -                               if lits = 1 
    1.82 -                               then
    1.83 -                                            
    1.84 -                                  contra
    1.85 -                               else
    1.86 -                                  rotate_prems (lits - n) contra
    1.87 -                          end
    1.88 -
    1.89 -
    1.90 -
    1.91 -fun zip xs [] = []
    1.92 -|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
    1.93 -
    1.94 -
    1.95 -fun unzip [] = ([],[])
    1.96 -    | unzip((x,y)::pairs) =
    1.97 -	  let val (xs,ys) = unzip pairs
    1.98 -	  in  (x::xs, y::ys)  end;
    1.99 -
   1.100 -fun numlist 0 = []
   1.101 -|   numlist n = (numlist (n - 1))@[n]
   1.102 -
   1.103 -
   1.104 -
   1.105 -
   1.106 -fun last(x::xs) = if xs=[] then x else last xs
   1.107 -fun butlast []= []
   1.108 -|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
   1.109 -
   1.110 -
   1.111 -fun minus a b = b - a;
   1.112 -
   1.113 -
   1.114 -
   1.115 -
   1.116 -(* gives meta clause with kth disj as concl (starting at 1) *)
   1.117 -(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules  th)
   1.118 -         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
   1.119 -
   1.120 -
   1.121 -(* get a meta-clause for resolution with correct order of literals *)
   1.122 -fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
   1.123 -                                   val contra =  if lits = 1 
   1.124 -                                                 then
   1.125 -                                                     th
   1.126 -                                                 else
   1.127 -                                                     rots (n,th)   
   1.128 -                                in 
   1.129 -                                   if lits = 1 
   1.130 -                                   then
   1.131 -                                            
   1.132 -                                     contra
   1.133 -                                   else
   1.134 -                                     rotate_prems (lits - n) contra
   1.135 -                               end
   1.136 -*)
   1.137 -
   1.138 -
   1.139 -
   1.140  
   1.141  fun zip xs [] = []
   1.142  |   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))