src/HOL/Tools/ATP/recon_order_clauses.ML
author quigley
Thu Mar 31 19:29:26 2005 +0200 (2005-03-31)
changeset 15642 028059faa963
child 15684 5ec4d21889d6
permissions -rw-r--r--
*** empty log message ***
quigley@15642
     1
quigley@15642
     2
quigley@15642
     3
(*----------------------------------------------*)
quigley@15642
     4
(* Reorder clauses for use in binary resolution *)
quigley@15642
     5
(*----------------------------------------------*)
quigley@15642
     6
fun take n [] = []
quigley@15642
     7
|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
quigley@15642
     8
quigley@15642
     9
fun drop n [] = []
quigley@15642
    10
|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
quigley@15642
    11
quigley@15642
    12
fun remove n [] = []
quigley@15642
    13
|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
quigley@15642
    14
quigley@15642
    15
fun remove_nth n [] = []
quigley@15642
    16
|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
quigley@15642
    17
quigley@15642
    18
fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
quigley@15642
    19
quigley@15642
    20
quigley@15642
    21
 fun literals (Const("Trueprop",_) $ P) = literals P
quigley@15642
    22
   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
quigley@15642
    23
   | literals (Const("Not",_) $ P) = [(false,P)]
quigley@15642
    24
   | literals P = [(true,P)];
quigley@15642
    25
quigley@15642
    26
 (*number of literals in a term*)
quigley@15642
    27
 val nliterals = length o literals; 
quigley@15642
    28
     
quigley@15642
    29
exception Not_in_list;  
quigley@15642
    30
quigley@15642
    31
quigley@15642
    32
quigley@15642
    33
quigley@15642
    34
   (* get the literals from a disjunctive clause *)
quigley@15642
    35
quigley@15642
    36
(*fun get_disj_literals t = if is_disj t then
quigley@15642
    37
			           let 
quigley@15642
    38
                                      val {disj1, disj2} = dest_disj t  
quigley@15642
    39
                                   in 
quigley@15642
    40
                                      disj1::(get_disj_literals disj2)
quigley@15642
    41
                                   end
quigley@15642
    42
                                else
quigley@15642
    43
                                    ([t])
quigley@15642
    44
   
quigley@15642
    45
*)
quigley@15642
    46
             
quigley@15642
    47
(*
quigley@15642
    48
(* gives horn clause with kth disj as concl (starting at 1) *)
quigley@15642
    49
fun rots (0,th) =  (Meson.make_horn Meson.crules th)
quigley@15642
    50
         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
quigley@15642
    51
quigley@15642
    52
quigley@15642
    53
                
quigley@15642
    54
Goal " (~~P) == P";
quigley@15642
    55
by Auto_tac;
quigley@15642
    56
qed "notnotEq";
quigley@15642
    57
quigley@15642
    58
Goal "A | A ==> A";
quigley@15642
    59
by Auto_tac;
quigley@15642
    60
qed "rem_dup_disj";
quigley@15642
    61
quigley@15642
    62
quigley@15642
    63
quigley@15642
    64
quigley@15642
    65
(* New Meson code  Versions of make_neg_rule and make_pos_rule that don't insert new *)
quigley@15642
    66
(* assumptions, for ordinary resolution. *)
quigley@15642
    67
quigley@15642
    68
quigley@15642
    69
quigley@15642
    70
quigley@15642
    71
 val not_conjD = thm "meson_not_conjD";
quigley@15642
    72
 val not_disjD = thm "meson_not_disjD";
quigley@15642
    73
 val not_notD = thm "meson_not_notD";
quigley@15642
    74
 val not_allD = thm "meson_not_allD";
quigley@15642
    75
 val not_exD = thm "meson_not_exD";
quigley@15642
    76
 val imp_to_disjD = thm "meson_imp_to_disjD";
quigley@15642
    77
 val not_impD = thm "meson_not_impD";
quigley@15642
    78
 val iff_to_disjD = thm "meson_iff_to_disjD";
quigley@15642
    79
 val not_iffD = thm "meson_not_iffD";
quigley@15642
    80
 val conj_exD1 = thm "meson_conj_exD1";
quigley@15642
    81
 val conj_exD2 = thm "meson_conj_exD2";
quigley@15642
    82
 val disj_exD = thm "meson_disj_exD";
quigley@15642
    83
 val disj_exD1 = thm "meson_disj_exD1";
quigley@15642
    84
 val disj_exD2 = thm "meson_disj_exD2";
quigley@15642
    85
 val disj_assoc = thm "meson_disj_assoc";
quigley@15642
    86
 val disj_comm = thm "meson_disj_comm";
quigley@15642
    87
 val disj_FalseD1 = thm "meson_disj_FalseD1";
quigley@15642
    88
 val disj_FalseD2 = thm "meson_disj_FalseD2";
quigley@15642
    89
quigley@15642
    90
quigley@15642
    91
 fun literals (Const("Trueprop",_) $ P) = literals P
quigley@15642
    92
   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
quigley@15642
    93
   | literals (Const("Not",_) $ P) = [(false,P)]
quigley@15642
    94
   | literals P = [(true,P)];
quigley@15642
    95
quigley@15642
    96
 (*number of literals in a term*)
quigley@15642
    97
 val nliterals = length o literals; 
quigley@15642
    98
     
quigley@15642
    99
exception Not_in_list;  
quigley@15642
   100
quigley@15642
   101
quigley@15642
   102
(*Permute a rule's premises to move the i-th premise to the last position.*)
quigley@15642
   103
fun make_last i th =
quigley@15642
   104
  let val n = nprems_of th 
quigley@15642
   105
  in  if 1 <= i andalso i <= n 
quigley@15642
   106
      then Thm.permute_prems (i-1) 1 th
quigley@15642
   107
      else raise THM("make_last", i, [th])
quigley@15642
   108
  end;
quigley@15642
   109
quigley@15642
   110
(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
quigley@15642
   111
  double-negations.*)
quigley@15642
   112
val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection];
quigley@15642
   113
quigley@15642
   114
(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
quigley@15642
   115
fun select_literal i cl = negate_head (make_last i cl);
quigley@15642
   116
quigley@15642
   117
quigley@15642
   118
(* get a meta-clause for resolution with correct order of literals *)
quigley@15642
   119
fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
quigley@15642
   120
                              val contra =  if lits = 1 
quigley@15642
   121
                                                 then
quigley@15642
   122
                                                     th
quigley@15642
   123
                                                 else
quigley@15642
   124
                                                     rots (n,th)   
quigley@15642
   125
                          in 
quigley@15642
   126
                               if lits = 1 
quigley@15642
   127
                               then
quigley@15642
   128
                                            
quigley@15642
   129
                                  contra
quigley@15642
   130
                               else
quigley@15642
   131
                                  rotate_prems (lits - n) contra
quigley@15642
   132
                          end
quigley@15642
   133
quigley@15642
   134
quigley@15642
   135
quigley@15642
   136
quigley@15642
   137
quigley@15642
   138
quigley@15642
   139
quigley@15642
   140
fun zip xs [] = []
quigley@15642
   141
|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
quigley@15642
   142
quigley@15642
   143
quigley@15642
   144
fun unzip [] = ([],[])
quigley@15642
   145
    | unzip((x,y)::pairs) =
quigley@15642
   146
	  let val (xs,ys) = unzip pairs
quigley@15642
   147
	  in  (x::xs, y::ys)  end;
quigley@15642
   148
quigley@15642
   149
fun numlist 0 = []
quigley@15642
   150
|   numlist n = (numlist (n - 1))@[n]
quigley@15642
   151
quigley@15642
   152
quigley@15642
   153
fun is_abs t = can dest_abs t;
quigley@15642
   154
fun is_comb t = can dest_comb t;
quigley@15642
   155
quigley@15642
   156
fun iscomb a = if is_Free a then
quigley@15642
   157
			false
quigley@15642
   158
	      else if is_Var a then
quigley@15642
   159
			false
quigley@15642
   160
		else if is_conj a then
quigley@15642
   161
			false
quigley@15642
   162
		else if is_disj a then
quigley@15642
   163
			false
quigley@15642
   164
		else if is_forall a then
quigley@15642
   165
			false
quigley@15642
   166
		else if is_exists a then
quigley@15642
   167
			false
quigley@15642
   168
		else
quigley@15642
   169
			true;
quigley@15642
   170
quigley@15642
   171
quigley@15642
   172
quigley@15642
   173
quigley@15642
   174
fun last(x::xs) = if xs=[] then x else last xs
quigley@15642
   175
fun butlast []= []
quigley@15642
   176
|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
quigley@15642
   177
quigley@15642
   178
quigley@15642
   179
fun minus a b = b - a;
quigley@15642
   180
quigley@15642
   181
quigley@15642
   182
quigley@15642
   183
quigley@15642
   184
(* gives meta clause with kth disj as concl (starting at 1) *)
quigley@15642
   185
(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules  th)
quigley@15642
   186
         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
quigley@15642
   187
quigley@15642
   188
quigley@15642
   189
(* get a meta-clause for resolution with correct order of literals *)
quigley@15642
   190
fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
quigley@15642
   191
                                   val contra =  if lits = 1 
quigley@15642
   192
                                                 then
quigley@15642
   193
                                                     th
quigley@15642
   194
                                                 else
quigley@15642
   195
                                                     rots (n,th)   
quigley@15642
   196
                                in 
quigley@15642
   197
                                   if lits = 1 
quigley@15642
   198
                                   then
quigley@15642
   199
                                            
quigley@15642
   200
                                     contra
quigley@15642
   201
                                   else
quigley@15642
   202
                                     rotate_prems (lits - n) contra
quigley@15642
   203
                               end
quigley@15642
   204
*)
quigley@15642
   205
quigley@15642
   206
quigley@15642
   207
quigley@15642
   208
quigley@15642
   209
fun zip xs [] = []
quigley@15642
   210
|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
quigley@15642
   211
quigley@15642
   212
quigley@15642
   213
fun unzip [] = ([],[])
quigley@15642
   214
    | unzip((x,y)::pairs) =
quigley@15642
   215
	  let val (xs,ys) = unzip pairs
quigley@15642
   216
	  in  (x::xs, y::ys)  end;
quigley@15642
   217
quigley@15642
   218
fun numlist 0 = []
quigley@15642
   219
|   numlist n = (numlist (n - 1))@[n]
quigley@15642
   220
quigley@15642
   221
quigley@15642
   222
fun is_abs t = can dest_abs t;
quigley@15642
   223
fun is_comb t = can dest_comb t;
quigley@15642
   224
quigley@15642
   225
fun iscomb a = if is_Free a then
quigley@15642
   226
			false
quigley@15642
   227
	      else if is_Var a then
quigley@15642
   228
			false
quigley@15642
   229
		else if is_conj a then
quigley@15642
   230
			false
quigley@15642
   231
		else if is_disj a then
quigley@15642
   232
			false
quigley@15642
   233
		else if is_forall a then
quigley@15642
   234
			false
quigley@15642
   235
		else if is_exists a then
quigley@15642
   236
			false
quigley@15642
   237
		else
quigley@15642
   238
			true;
quigley@15642
   239
quigley@15642
   240
quigley@15642
   241
quigley@15642
   242
quigley@15642
   243
fun last(x::xs) = if xs=[] then x else last xs
quigley@15642
   244
fun butlast []= []
quigley@15642
   245
|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
quigley@15642
   246
quigley@15642
   247
quigley@15642
   248
fun minus a b = b - a;
quigley@15642
   249
quigley@15642
   250
quigley@15642
   251
(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
quigley@15642
   252
quigley@15642
   253
fun assoc3 a [] = raise Noassoc
quigley@15642
   254
  | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
quigley@15642
   255
quigley@15642
   256
quigley@15642
   257
fun third (a,b,c) = c;
quigley@15642
   258
quigley@15642
   259
quigley@15642
   260
 fun takeUntil ch [] res  = (res, [])
quigley@15642
   261
 |   takeUntil ch (x::xs) res = if   x = ch 
quigley@15642
   262
                                then
quigley@15642
   263
                                     (res, xs)
quigley@15642
   264
                                else
quigley@15642
   265
                                     takeUntil ch xs (res@[x])
quigley@15642
   266
fun contains_eq str = inlist "=" str 
quigley@15642
   267
quigley@15642
   268
fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
quigley@15642
   269
                     in
quigley@15642
   270
                        if ((last uptoeq) = "~")
quigley@15642
   271
                        then 
quigley@15642
   272
                            false
quigley@15642
   273
                        else
quigley@15642
   274
                            true
quigley@15642
   275
                     end
quigley@15642
   276
                   
quigley@15642
   277
quigley@15642
   278
quigley@15642
   279
quigley@15642
   280
fun get_eq_strs str =  if eq_not_neq  str   (*not an inequality *)
quigley@15642
   281
                       then 
quigley@15642
   282
                           let val (left, right) = takeUntil "=" str []
quigley@15642
   283
                           in
quigley@15642
   284
                               ((butlast left), (drop 1 right))
quigley@15642
   285
                           end
quigley@15642
   286
                       else                  (* is an inequality *)
quigley@15642
   287
                           let val (left, right) = takeUntil "~" str []
quigley@15642
   288
                           in 
quigley@15642
   289
                              ((butlast left), (drop 2 right))
quigley@15642
   290
                           end
quigley@15642
   291
                
quigley@15642
   292
quigley@15642
   293
quigley@15642
   294
fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
quigley@15642
   295
                           val (x_lhs, x_rhs) = get_eq_strs x
quigley@15642
   296
quigley@15642
   297
                       in
quigley@15642
   298
                           (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
quigley@15642
   299
                       end
quigley@15642
   300
quigley@15642
   301
fun equal_pair (a,b) = equal a b
quigley@15642
   302
quigley@15642
   303
fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
quigley@15642
   304
quigley@15642
   305
fun var_equiv vars (a,b)  = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
quigley@15642
   306
quigley@15642
   307
fun all_true [] = false
quigley@15642
   308
|   all_true xs = let val falselist = List.filter (equal false ) xs 
quigley@15642
   309
                  in
quigley@15642
   310
                      falselist = []
quigley@15642
   311
                  end
quigley@15642
   312
quigley@15642
   313
quigley@15642
   314
quigley@15642
   315
fun var_pos_eq vars x y = let val xs = explode x
quigley@15642
   316
                              val ys = explode y
quigley@15642
   317
                          in
quigley@15642
   318
                              if not_equal (length xs) (length ys)
quigley@15642
   319
                              then 
quigley@15642
   320
                                  false
quigley@15642
   321
                              else
quigley@15642
   322
                                  let val xsys = zip xs ys
quigley@15642
   323
                                      val are_var_pairs = map (var_equiv vars) xsys
quigley@15642
   324
                                  in
quigley@15642
   325
                                      all_true are_var_pairs 
quigley@15642
   326
                                  end
quigley@15642
   327
                          end
quigley@15642
   328
quigley@15642
   329
quigley@15642
   330
quigley@15642
   331
quigley@15642
   332
fun  pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
quigley@15642
   333
    |pos_in_list a (x::[])  allvars (pos_num , symlist, nsymlist) = 
quigley@15642
   334
                                 let val y = explode x 
quigley@15642
   335
                                     val b = explode a
quigley@15642
   336
                                 in
quigley@15642
   337
                                    if  b = y
quigley@15642
   338
                                    then 
quigley@15642
   339
                                         (pos_num, symlist, nsymlist)
quigley@15642
   340
                                    else 
quigley@15642
   341
                                         if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
quigley@15642
   342
                                         then 
quigley@15642
   343
                                             (pos_num, symlist, nsymlist)
quigley@15642
   344
                                         else 
quigley@15642
   345
                                             if (contains_eq b) andalso (contains_eq y)
quigley@15642
   346
                                             then 
quigley@15642
   347
                                                 if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
quigley@15642
   348
                                                 then 
quigley@15642
   349
                                                     (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
quigley@15642
   350
                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
quigley@15642
   351
                                                      then 
quigley@15642
   352
                                                          (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
quigley@15642
   353
                                                      else 
quigley@15642
   354
                                                           raise Not_in_list
quigley@15642
   355
                                             else 
quigley@15642
   356
                                                  raise Not_in_list
quigley@15642
   357
                                              
quigley@15642
   358
                                 end   
quigley@15642
   359
                                 
quigley@15642
   360
    | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = 
quigley@15642
   361
                                 let val y = explode x 
quigley@15642
   362
                                     val b = explode a
quigley@15642
   363
                                 in
quigley@15642
   364
                                    if  b = y
quigley@15642
   365
                                    then 
quigley@15642
   366
                                         (pos_num, symlist, nsymlist)
quigley@15642
   367
                                    
quigley@15642
   368
                                    else
quigley@15642
   369
                                          if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
quigley@15642
   370
                                          then 
quigley@15642
   371
                                             (pos_num, symlist, nsymlist)
quigley@15642
   372
                                          else 
quigley@15642
   373
                                              if (contains_eq b) andalso (contains_eq y)
quigley@15642
   374
                                              then 
quigley@15642
   375
                                                  if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
quigley@15642
   376
                                                  then 
quigley@15642
   377
                                                      (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
quigley@15642
   378
                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
quigley@15642
   379
                                                      then 
quigley@15642
   380
                                                           (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
quigley@15642
   381
                                                      else 
quigley@15642
   382
                                                           pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
quigley@15642
   383
                                              else 
quigley@15642
   384
                                                    pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
quigley@15642
   385
                                              
quigley@15642
   386
                                 end   
quigley@15642
   387
quigley@15642
   388
quigley@15642
   389
quigley@15642
   390
quigley@15642
   391
quigley@15642
   392
quigley@15642
   393
quigley@15642
   394
                                (* in
quigley@15642
   395
                                    if  b = y
quigley@15642
   396
                                    then 
quigley@15642
   397
                                         (pos_num, symlist, nsymlist)
quigley@15642
   398
                                    else if (contains_eq b) andalso (contains_eq y)
quigley@15642
   399
                                         then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
quigley@15642
   400
                                              then if (switch_equal b y )              (* if they're equal under sym *)
quigley@15642
   401
                                                   then 
quigley@15642
   402
                                                       (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)
quigley@15642
   403
                                                   else 
quigley@15642
   404
                                                         pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   405
                                              else if not(eq_not_neq b) andalso not(eq_not_neq y)  (* both are inequalities *)
quigley@15642
   406
                                                   then if (switch_equal b y )  (* if they're equal under not_sym *)
quigley@15642
   407
                                                        then 
quigley@15642
   408
                                                            (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
quigley@15642
   409
                                                        else 
quigley@15642
   410
                                                                 pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   411
                                                   else
quigley@15642
   412
                                                          pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   413
                                               else  
quigley@15642
   414
                                                       pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   415
                                          else 
quigley@15642
   416
                                                  pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   417
                                 end   
quigley@15642
   418
quigley@15642
   419
                                *)
quigley@15642
   420
quigley@15642
   421
quigley@15642
   422
quigley@15642
   423
quigley@15642
   424
quigley@15642
   425
quigley@15642
   426
quigley@15642
   427
quigley@15642
   428
quigley@15642
   429
quigley@15642
   430
(* checkorder Spass Isabelle [] *)
quigley@15642
   431
quigley@15642
   432
fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
quigley@15642
   433
|   checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =  
quigley@15642
   434
         let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist) 
quigley@15642
   435
         in
quigley@15642
   436
             checkorder xs  strlist allvars ((numlist@[posnum]), symlist', not_symlist') 
quigley@15642
   437
         end
quigley@15642
   438
quigley@15642
   439
fun is_digit ch =
quigley@15642
   440
    ( ch >=  "0" andalso ch <=  "9")
quigley@15642
   441
quigley@15642
   442
quigley@15642
   443
fun is_alpha ch =
quigley@15642
   444
    (ch >=  "A" andalso  ch <=  "Z") orelse
quigley@15642
   445
    (ch >=  "a" andalso ch <=  "z")
quigley@15642
   446
quigley@15642
   447
quigley@15642
   448
fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
quigley@15642
   449
quigley@15642
   450
fun lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t
quigley@15642
   451
                       val exp_term = explode termstr
quigley@15642
   452
                   in
quigley@15642
   453
                       implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
quigley@15642
   454
                   end
quigley@15642
   455
quigley@15642
   456
fun get_meta_lits thm = map lit_string (prems_of thm)
quigley@15642
   457
quigley@15642
   458
quigley@15642
   459
quigley@15642
   460
quigley@15642
   461
fun is_alpha_space_or_neg_or_eq_or_bracket ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=") orelse (ch= "(") orelse (ch = ")")
quigley@15642
   462
quigley@15642
   463
fun lit_string_bracket  t = let val termstr = (Sign.string_of_term Mainsign ) t
quigley@15642
   464
                       val exp_term = explode termstr
quigley@15642
   465
                   in
quigley@15642
   466
                       implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
quigley@15642
   467
                   end
quigley@15642
   468
quigley@15642
   469
fun get_meta_lits_bracket thm = map lit_string_bracket (prems_of thm)
quigley@15642
   470
quigley@15642
   471
quigley@15642
   472
quigley@15642
   473
      
quigley@15642
   474
fun apply_rule rule [] thm = thm
quigley@15642
   475
|   apply_rule rule  (x::xs) thm = let val thm' = rule RSN ((x+1),thm)
quigley@15642
   476
                                  in
quigley@15642
   477
                                      apply_rule rule xs thm'
quigley@15642
   478
                                  end
quigley@15642
   479
quigley@15642
   480
quigley@15642
   481
quigley@15642
   482
                    (* resulting thm, clause-strs in spass order, vars *)
quigley@15642
   483
quigley@15642
   484
fun rearrange_clause thm res_strlist allvars = 
quigley@15642
   485
                          let val isa_strlist = get_meta_lits thm
quigley@15642
   486
                              val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
quigley@15642
   487
                              val symmed = apply_rule sym symlist thm
quigley@15642
   488
                              val not_symmed = apply_rule not_sym not_symlist symmed
quigley@15642
   489
                                           
quigley@15642
   490
                          in
quigley@15642
   491
                             ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
quigley@15642
   492
                          end