src/HOL/Tools/ATP/recon_order_clauses.ML
changeset 15642 028059faa963
child 15684 5ec4d21889d6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Thu Mar 31 19:29:26 2005 +0200
     1.3 @@ -0,0 +1,492 @@
     1.4 +
     1.5 +
     1.6 +(*----------------------------------------------*)
     1.7 +(* Reorder clauses for use in binary resolution *)
     1.8 +(*----------------------------------------------*)
     1.9 +fun take n [] = []
    1.10 +|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
    1.11 +
    1.12 +fun drop n [] = []
    1.13 +|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
    1.14 +
    1.15 +fun remove n [] = []
    1.16 +|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
    1.17 +
    1.18 +fun remove_nth n [] = []
    1.19 +|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
    1.20 +
    1.21 +fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
    1.22 +
    1.23 +
    1.24 + fun literals (Const("Trueprop",_) $ P) = literals P
    1.25 +   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
    1.26 +   | literals (Const("Not",_) $ P) = [(false,P)]
    1.27 +   | literals P = [(true,P)];
    1.28 +
    1.29 + (*number of literals in a term*)
    1.30 + val nliterals = length o literals; 
    1.31 +     
    1.32 +exception Not_in_list;  
    1.33 +
    1.34 +
    1.35 +
    1.36 +
    1.37 +   (* get the literals from a disjunctive clause *)
    1.38 +
    1.39 +(*fun get_disj_literals t = if is_disj t then
    1.40 +			           let 
    1.41 +                                      val {disj1, disj2} = dest_disj t  
    1.42 +                                   in 
    1.43 +                                      disj1::(get_disj_literals disj2)
    1.44 +                                   end
    1.45 +                                else
    1.46 +                                    ([t])
    1.47 +   
    1.48 +*)
    1.49 +             
    1.50 +(*
    1.51 +(* gives horn clause with kth disj as concl (starting at 1) *)
    1.52 +fun rots (0,th) =  (Meson.make_horn Meson.crules th)
    1.53 +         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
    1.54 +
    1.55 +
    1.56 +                
    1.57 +Goal " (~~P) == P";
    1.58 +by Auto_tac;
    1.59 +qed "notnotEq";
    1.60 +
    1.61 +Goal "A | A ==> A";
    1.62 +by Auto_tac;
    1.63 +qed "rem_dup_disj";
    1.64 +
    1.65 +
    1.66 +
    1.67 +
    1.68 +(* New Meson code  Versions of make_neg_rule and make_pos_rule that don't insert new *)
    1.69 +(* assumptions, for ordinary resolution. *)
    1.70 +
    1.71 +
    1.72 +
    1.73 +
    1.74 + val not_conjD = thm "meson_not_conjD";
    1.75 + val not_disjD = thm "meson_not_disjD";
    1.76 + val not_notD = thm "meson_not_notD";
    1.77 + val not_allD = thm "meson_not_allD";
    1.78 + val not_exD = thm "meson_not_exD";
    1.79 + val imp_to_disjD = thm "meson_imp_to_disjD";
    1.80 + val not_impD = thm "meson_not_impD";
    1.81 + val iff_to_disjD = thm "meson_iff_to_disjD";
    1.82 + val not_iffD = thm "meson_not_iffD";
    1.83 + val conj_exD1 = thm "meson_conj_exD1";
    1.84 + val conj_exD2 = thm "meson_conj_exD2";
    1.85 + val disj_exD = thm "meson_disj_exD";
    1.86 + val disj_exD1 = thm "meson_disj_exD1";
    1.87 + val disj_exD2 = thm "meson_disj_exD2";
    1.88 + val disj_assoc = thm "meson_disj_assoc";
    1.89 + val disj_comm = thm "meson_disj_comm";
    1.90 + val disj_FalseD1 = thm "meson_disj_FalseD1";
    1.91 + val disj_FalseD2 = thm "meson_disj_FalseD2";
    1.92 +
    1.93 +
    1.94 + fun literals (Const("Trueprop",_) $ P) = literals P
    1.95 +   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
    1.96 +   | literals (Const("Not",_) $ P) = [(false,P)]
    1.97 +   | literals P = [(true,P)];
    1.98 +
    1.99 + (*number of literals in a term*)
   1.100 + val nliterals = length o literals; 
   1.101 +     
   1.102 +exception Not_in_list;  
   1.103 +
   1.104 +
   1.105 +(*Permute a rule's premises to move the i-th premise to the last position.*)
   1.106 +fun make_last i th =
   1.107 +  let val n = nprems_of th 
   1.108 +  in  if 1 <= i andalso i <= n 
   1.109 +      then Thm.permute_prems (i-1) 1 th
   1.110 +      else raise THM("make_last", i, [th])
   1.111 +  end;
   1.112 +
   1.113 +(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   1.114 +  double-negations.*)
   1.115 +val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
   1.116 +
   1.117 +(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
   1.118 +fun select_literal i cl = negate_head (make_last i cl);
   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 +
   1.142 +
   1.143 +fun zip xs [] = []
   1.144 +|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
   1.145 +
   1.146 +
   1.147 +fun unzip [] = ([],[])
   1.148 +    | unzip((x,y)::pairs) =
   1.149 +	  let val (xs,ys) = unzip pairs
   1.150 +	  in  (x::xs, y::ys)  end;
   1.151 +
   1.152 +fun numlist 0 = []
   1.153 +|   numlist n = (numlist (n - 1))@[n]
   1.154 +
   1.155 +
   1.156 +fun is_abs t = can dest_abs t;
   1.157 +fun is_comb t = can dest_comb t;
   1.158 +
   1.159 +fun iscomb a = if is_Free a then
   1.160 +			false
   1.161 +	      else if is_Var a then
   1.162 +			false
   1.163 +		else if is_conj a then
   1.164 +			false
   1.165 +		else if is_disj a then
   1.166 +			false
   1.167 +		else if is_forall a then
   1.168 +			false
   1.169 +		else if is_exists a then
   1.170 +			false
   1.171 +		else
   1.172 +			true;
   1.173 +
   1.174 +
   1.175 +
   1.176 +
   1.177 +fun last(x::xs) = if xs=[] then x else last xs
   1.178 +fun butlast []= []
   1.179 +|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
   1.180 +
   1.181 +
   1.182 +fun minus a b = b - a;
   1.183 +
   1.184 +
   1.185 +
   1.186 +
   1.187 +(* gives meta clause with kth disj as concl (starting at 1) *)
   1.188 +(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules  th)
   1.189 +         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
   1.190 +
   1.191 +
   1.192 +(* get a meta-clause for resolution with correct order of literals *)
   1.193 +fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
   1.194 +                                   val contra =  if lits = 1 
   1.195 +                                                 then
   1.196 +                                                     th
   1.197 +                                                 else
   1.198 +                                                     rots (n,th)   
   1.199 +                                in 
   1.200 +                                   if lits = 1 
   1.201 +                                   then
   1.202 +                                            
   1.203 +                                     contra
   1.204 +                                   else
   1.205 +                                     rotate_prems (lits - n) contra
   1.206 +                               end
   1.207 +*)
   1.208 +
   1.209 +
   1.210 +
   1.211 +
   1.212 +fun zip xs [] = []
   1.213 +|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
   1.214 +
   1.215 +
   1.216 +fun unzip [] = ([],[])
   1.217 +    | unzip((x,y)::pairs) =
   1.218 +	  let val (xs,ys) = unzip pairs
   1.219 +	  in  (x::xs, y::ys)  end;
   1.220 +
   1.221 +fun numlist 0 = []
   1.222 +|   numlist n = (numlist (n - 1))@[n]
   1.223 +
   1.224 +
   1.225 +fun is_abs t = can dest_abs t;
   1.226 +fun is_comb t = can dest_comb t;
   1.227 +
   1.228 +fun iscomb a = if is_Free a then
   1.229 +			false
   1.230 +	      else if is_Var a then
   1.231 +			false
   1.232 +		else if is_conj a then
   1.233 +			false
   1.234 +		else if is_disj a then
   1.235 +			false
   1.236 +		else if is_forall a then
   1.237 +			false
   1.238 +		else if is_exists a then
   1.239 +			false
   1.240 +		else
   1.241 +			true;
   1.242 +
   1.243 +
   1.244 +
   1.245 +
   1.246 +fun last(x::xs) = if xs=[] then x else last xs
   1.247 +fun butlast []= []
   1.248 +|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
   1.249 +
   1.250 +
   1.251 +fun minus a b = b - a;
   1.252 +
   1.253 +
   1.254 +(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
   1.255 +
   1.256 +fun assoc3 a [] = raise Noassoc
   1.257 +  | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
   1.258 +
   1.259 +
   1.260 +fun third (a,b,c) = c;
   1.261 +
   1.262 +
   1.263 + fun takeUntil ch [] res  = (res, [])
   1.264 + |   takeUntil ch (x::xs) res = if   x = ch 
   1.265 +                                then
   1.266 +                                     (res, xs)
   1.267 +                                else
   1.268 +                                     takeUntil ch xs (res@[x])
   1.269 +fun contains_eq str = inlist "=" str 
   1.270 +
   1.271 +fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
   1.272 +                     in
   1.273 +                        if ((last uptoeq) = "~")
   1.274 +                        then 
   1.275 +                            false
   1.276 +                        else
   1.277 +                            true
   1.278 +                     end
   1.279 +                   
   1.280 +
   1.281 +
   1.282 +
   1.283 +fun get_eq_strs str =  if eq_not_neq  str   (*not an inequality *)
   1.284 +                       then 
   1.285 +                           let val (left, right) = takeUntil "=" str []
   1.286 +                           in
   1.287 +                               ((butlast left), (drop 1 right))
   1.288 +                           end
   1.289 +                       else                  (* is an inequality *)
   1.290 +                           let val (left, right) = takeUntil "~" str []
   1.291 +                           in 
   1.292 +                              ((butlast left), (drop 2 right))
   1.293 +                           end
   1.294 +                
   1.295 +
   1.296 +
   1.297 +fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
   1.298 +                           val (x_lhs, x_rhs) = get_eq_strs x
   1.299 +
   1.300 +                       in
   1.301 +                           (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
   1.302 +                       end
   1.303 +
   1.304 +fun equal_pair (a,b) = equal a b
   1.305 +
   1.306 +fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
   1.307 +
   1.308 +fun var_equiv vars (a,b)  = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
   1.309 +
   1.310 +fun all_true [] = false
   1.311 +|   all_true xs = let val falselist = List.filter (equal false ) xs 
   1.312 +                  in
   1.313 +                      falselist = []
   1.314 +                  end
   1.315 +
   1.316 +
   1.317 +
   1.318 +fun var_pos_eq vars x y = let val xs = explode x
   1.319 +                              val ys = explode y
   1.320 +                          in
   1.321 +                              if not_equal (length xs) (length ys)
   1.322 +                              then 
   1.323 +                                  false
   1.324 +                              else
   1.325 +                                  let val xsys = zip xs ys
   1.326 +                                      val are_var_pairs = map (var_equiv vars) xsys
   1.327 +                                  in
   1.328 +                                      all_true are_var_pairs 
   1.329 +                                  end
   1.330 +                          end
   1.331 +
   1.332 +
   1.333 +
   1.334 +
   1.335 +fun  pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
   1.336 +    |pos_in_list a (x::[])  allvars (pos_num , symlist, nsymlist) = 
   1.337 +                                 let val y = explode x 
   1.338 +                                     val b = explode a
   1.339 +                                 in
   1.340 +                                    if  b = y
   1.341 +                                    then 
   1.342 +                                         (pos_num, symlist, nsymlist)
   1.343 +                                    else 
   1.344 +                                         if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
   1.345 +                                         then 
   1.346 +                                             (pos_num, symlist, nsymlist)
   1.347 +                                         else 
   1.348 +                                             if (contains_eq b) andalso (contains_eq y)
   1.349 +                                             then 
   1.350 +                                                 if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
   1.351 +                                                 then 
   1.352 +                                                     (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
   1.353 +                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
   1.354 +                                                      then 
   1.355 +                                                          (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.356 +                                                      else 
   1.357 +                                                           raise Not_in_list
   1.358 +                                             else 
   1.359 +                                                  raise Not_in_list
   1.360 +                                              
   1.361 +                                 end   
   1.362 +                                 
   1.363 +    | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = 
   1.364 +                                 let val y = explode x 
   1.365 +                                     val b = explode a
   1.366 +                                 in
   1.367 +                                    if  b = y
   1.368 +                                    then 
   1.369 +                                         (pos_num, symlist, nsymlist)
   1.370 +                                    
   1.371 +                                    else
   1.372 +                                          if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
   1.373 +                                          then 
   1.374 +                                             (pos_num, symlist, nsymlist)
   1.375 +                                          else 
   1.376 +                                              if (contains_eq b) andalso (contains_eq y)
   1.377 +                                              then 
   1.378 +                                                  if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
   1.379 +                                                  then 
   1.380 +                                                      (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
   1.381 +                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
   1.382 +                                                      then 
   1.383 +                                                           (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.384 +                                                      else 
   1.385 +                                                           pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   1.386 +                                              else 
   1.387 +                                                    pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   1.388 +                                              
   1.389 +                                 end   
   1.390 +
   1.391 +
   1.392 +
   1.393 +
   1.394 +
   1.395 +
   1.396 +
   1.397 +                                (* in
   1.398 +                                    if  b = y
   1.399 +                                    then 
   1.400 +                                         (pos_num, symlist, nsymlist)
   1.401 +                                    else if (contains_eq b) andalso (contains_eq y)
   1.402 +                                         then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
   1.403 +                                              then if (switch_equal b y )              (* if they're equal under sym *)
   1.404 +                                                   then 
   1.405 +                                                       (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)
   1.406 +                                                   else 
   1.407 +                                                         pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.408 +                                              else if not(eq_not_neq b) andalso not(eq_not_neq y)  (* both are inequalities *)
   1.409 +                                                   then if (switch_equal b y )  (* if they're equal under not_sym *)
   1.410 +                                                        then 
   1.411 +                                                            (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.412 +                                                        else 
   1.413 +                                                                 pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.414 +                                                   else
   1.415 +                                                          pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.416 +                                               else  
   1.417 +                                                       pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.418 +                                          else 
   1.419 +                                                  pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.420 +                                 end   
   1.421 +
   1.422 +                                *)
   1.423 +
   1.424 +
   1.425 +
   1.426 +
   1.427 +
   1.428 +
   1.429 +
   1.430 +
   1.431 +
   1.432 +
   1.433 +(* checkorder Spass Isabelle [] *)
   1.434 +
   1.435 +fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
   1.436 +|   checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =  
   1.437 +         let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist) 
   1.438 +         in
   1.439 +             checkorder xs  strlist allvars ((numlist@[posnum]), symlist', not_symlist') 
   1.440 +         end
   1.441 +
   1.442 +fun is_digit ch =
   1.443 +    ( ch >=  "0" andalso ch <=  "9")
   1.444 +
   1.445 +
   1.446 +fun is_alpha ch =
   1.447 +    (ch >=  "A" andalso  ch <=  "Z") orelse
   1.448 +    (ch >=  "a" andalso ch <=  "z")
   1.449 +
   1.450 +
   1.451 +fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
   1.452 +
   1.453 +fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
   1.454 +                       val exp_term = explode termstr
   1.455 +                   in
   1.456 +                       implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
   1.457 +                   end
   1.458 +
   1.459 +fun get_meta_lits thm = map lit_string (prems_of thm)
   1.460 +
   1.461 +
   1.462 +
   1.463 +
   1.464 +fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
   1.465 +
   1.466 +fun lit_string_bracket  t = let val termstr = (Sign.string_of_term Mainsign ) t
   1.467 +                       val exp_term = explode termstr
   1.468 +                   in
   1.469 +                       implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
   1.470 +                   end
   1.471 +
   1.472 +fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
   1.473 +
   1.474 +
   1.475 +
   1.476 +      
   1.477 +fun apply_rule rule [] thm = thm
   1.478 +|   apply_rule rule  (x::xs) thm = let val thm' = rule RSN ((x+1),thm)
   1.479 +                                  in
   1.480 +                                      apply_rule rule xs thm'
   1.481 +                                  end
   1.482 +
   1.483 +
   1.484 +
   1.485 +                    (* resulting thm, clause-strs in spass order, vars *)
   1.486 +
   1.487 +fun rearrange_clause thm res_strlist allvars = 
   1.488 +                          let val isa_strlist = get_meta_lits thm
   1.489 +                              val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
   1.490 +                              val symmed = apply_rule sym symlist thm
   1.491 +                              val not_symmed = apply_rule not_sym not_symlist symmed
   1.492 +                                           
   1.493 +                          in
   1.494 +                             ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
   1.495 +                          end