src/HOL/Tools/ATP/recon_translate_proof.ML
author quigley
Wed Apr 06 12:01:37 2005 +0200 (2005-04-06 ago)
changeset 15658 2edb384bf61f
parent 15642 028059faa963
child 15684 5ec4d21889d6
permissions -rw-r--r--
watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley@15642
     1
quigley@15642
     2
fun take n [] = []
quigley@15642
     3
|   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
quigley@15642
     4
quigley@15642
     5
fun drop n [] = []
quigley@15642
     6
|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
quigley@15642
     7
quigley@15642
     8
fun remove n [] = []
quigley@15642
     9
|   remove n (x::xs) = List.filter (not_equal n) (x::xs);
quigley@15642
    10
quigley@15642
    11
fun remove_nth n [] = []
quigley@15642
    12
|   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
quigley@15642
    13
quigley@15642
    14
fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
quigley@15642
    15
quigley@15642
    16
fun add_in_order (x:string) [] = [x]
quigley@15642
    17
|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
quigley@15642
    18
                             then 
quigley@15642
    19
                                  (x::(y::ys))
quigley@15642
    20
                             else
quigley@15642
    21
                                  (y::(add_in_order x ys))
quigley@15642
    22
fun add_once x [] = [x]
quigley@15642
    23
|   add_once x (y::ys) = if (inlist x (y::ys)) then 
quigley@15642
    24
                            (y::ys)
quigley@15642
    25
                        else
quigley@15642
    26
                            add_in_order x (y::ys)
quigley@15642
    27
     
quigley@15642
    28
fun thm_vars thm = map getindexstring (map fst (Drule.vars_of thm));
quigley@15642
    29
quigley@15642
    30
Goal "False ==> False";
quigley@15642
    31
by Auto_tac;
quigley@15642
    32
qed "False_imp";
quigley@15642
    33
quigley@15642
    34
exception Reflex_equal;
quigley@15642
    35
quigley@15642
    36
(********************************)
quigley@15642
    37
(* Proofstep datatype           *)
quigley@15642
    38
(********************************)
quigley@15642
    39
(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)
quigley@15642
    40
quigley@15642
    41
datatype Side = Left |Right
quigley@15642
    42
quigley@15642
    43
 datatype Proofstep = ExtraAxiom
quigley@15642
    44
                     |OrigAxiom
quigley@15642
    45
                     | Axiom
quigley@15642
    46
                     | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
quigley@15642
    47
                     | MRR of (int * int) * (int * int) 
quigley@15642
    48
                     | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
quigley@15642
    49
                     | Para of (int * int) * (int * int) 
quigley@15642
    50
                     | Rewrite of (int * int) * (int * int)  
quigley@15642
    51
                     | Obvious of (int * int)
quigley@15642
    52
                     (*| Hyper of int list*)
quigley@15642
    53
                     | Unusedstep of unit
quigley@15642
    54
quigley@15642
    55
quigley@15642
    56
datatype Clausesimp = Binary_s of int * int
quigley@15642
    57
                      | Factor_s of unit
quigley@15642
    58
                      | Demod_s of (int * int) list
quigley@15642
    59
                      | Hyper_s of int list
quigley@15642
    60
                      | Unusedstep_s of unit
quigley@15642
    61
quigley@15642
    62
quigley@15642
    63
quigley@15642
    64
datatype Step_label = T_info
quigley@15642
    65
                     |P_info
quigley@15642
    66
quigley@15642
    67
quigley@15642
    68
fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ")
quigley@15642
    69
quigley@15642
    70
quigley@15642
    71
quigley@15642
    72
fun lit_string_with_nums t = let val termstr = (Sign.string_of_term Mainsign) t
quigley@15642
    73
                                 val exp_term = explode termstr
quigley@15642
    74
                             in
quigley@15642
    75
                                 implode(List.filter is_alpha_space_digit_or_neg exp_term)
quigley@15642
    76
                             end
quigley@15642
    77
quigley@15642
    78
quigley@15642
    79
(****************************************)
quigley@15642
    80
(* Reconstruct an axiom resolution step *)
quigley@15642
    81
(****************************************)
quigley@15642
    82
quigley@15642
    83
 fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
quigley@15642
    84
                                     let val this_axiom =(assoc  clausenum clauses)
quigley@15642
    85
                                         val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)         
quigley@15642
    86
                                         val thmvars = thm_vars res
quigley@15642
    87
                                     in
quigley@15642
    88
                                         (res, (Axiom,clause_strs,thmvars )  )
quigley@15642
    89
                                     end
quigley@15642
    90
quigley@15642
    91
(****************************************)
quigley@15642
    92
(* Reconstruct a binary resolution step *)
quigley@15642
    93
(****************************************)
quigley@15642
    94
quigley@15642
    95
                 (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
quigley@15642
    96
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs 
quigley@15642
    97
        = let
quigley@15642
    98
              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
quigley@15642
    99
              val thm2 =  assoc  clause2 thml
quigley@15642
   100
              val res =   thm1 RSN ((lit2 +1), thm2)
quigley@15642
   101
              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
quigley@15642
   102
              val thmvars = thm_vars res
quigley@15642
   103
          in
quigley@15642
   104
             (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
quigley@15642
   105
          end
quigley@15642
   106
quigley@15642
   107
quigley@15642
   108
quigley@15642
   109
(******************************************************)
quigley@15642
   110
(* Reconstruct a matching replacement resolution step *)
quigley@15642
   111
(******************************************************)
quigley@15642
   112
quigley@15642
   113
quigley@15642
   114
fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs 
quigley@15642
   115
        = let
quigley@15642
   116
              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
quigley@15642
   117
              val thm2 =  assoc  clause2 thml
quigley@15642
   118
              val res =   thm1 RSN ((lit2 +1), thm2)
quigley@15642
   119
              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
quigley@15642
   120
              val thmvars = thm_vars res
quigley@15642
   121
          in
quigley@15642
   122
             (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
quigley@15642
   123
          end
quigley@15642
   124
quigley@15642
   125
quigley@15642
   126
(*******************************************)
quigley@15642
   127
(* Reconstruct a factoring resolution step *)
quigley@15642
   128
(*******************************************)
quigley@15642
   129
quigley@15642
   130
fun mksubstlist [] sublist = sublist
quigley@15642
   131
   |mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b 
quigley@15642
   132
                                          val avar = Var(a,vartype)
quigley@15642
   133
                                          val newlist = ((avar,b)::sublist) in
quigley@15642
   134
                                          mksubstlist rest newlist
quigley@15642
   135
                                      end;
quigley@15642
   136
quigley@15642
   137
(* based on Tactic.distinct_subgoals_tac *)
quigley@15642
   138
quigley@15642
   139
fun delete_assump_tac state lit =
quigley@15642
   140
    let val (frozth,thawfn) = freeze_thaw state
quigley@15642
   141
        val froz_prems = cprems_of frozth
quigley@15642
   142
        val assumed = implies_elim_list frozth (map assume froz_prems)
quigley@15642
   143
        val new_prems = remove_nth lit froz_prems
quigley@15642
   144
        val implied = implies_intr_list new_prems assumed
quigley@15642
   145
    in  
quigley@15642
   146
        Seq.single (thawfn implied)  
quigley@15642
   147
    end
quigley@15642
   148
quigley@15642
   149
quigley@15642
   150
quigley@15642
   151
quigley@15642
   152
quigley@15642
   153
(*************************************)
quigley@15642
   154
(* Reconstruct a factoring step      *)
quigley@15642
   155
(*************************************)
quigley@15642
   156
quigley@15642
   157
fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
quigley@15642
   158
                          let 
quigley@15642
   159
                            val th =  assoc clause thml
quigley@15642
   160
                            val prems = prems_of th
quigley@15642
   161
                            val fac1 = get_nth (lit1+1) prems
quigley@15642
   162
                            val fac2 = get_nth (lit2+1) prems
quigley@15642
   163
                            val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
quigley@15642
   164
                            val newenv = getnewenv unif_env
quigley@15642
   165
                            val envlist = alist_of newenv
quigley@15642
   166
                            
quigley@15642
   167
                            val newsubsts = mksubstlist envlist []
quigley@15642
   168
                          in 
quigley@15642
   169
                            if (is_Var (fst(hd(newsubsts))))
quigley@15642
   170
                            then
quigley@15642
   171
                                let 
quigley@15642
   172
                                   val str1 = lit_string_with_nums (fst (hd newsubsts));
quigley@15642
   173
                                   val str2 = lit_string_with_nums (snd (hd newsubsts));
quigley@15642
   174
                                   val facthm = read_instantiate [(str1,str2)] th;
quigley@15642
   175
                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
quigley@15642
   176
                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
quigley@15642
   177
                                   val thmvars = thm_vars res'
quigley@15642
   178
                                in 
quigley@15642
   179
                                       (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
quigley@15642
   180
                                end
quigley@15642
   181
                            else
quigley@15642
   182
                                let
quigley@15642
   183
                                   val str2 = lit_string_with_nums (fst (hd newsubsts));
quigley@15642
   184
                                   val str1 = lit_string_with_nums (snd (hd newsubsts));
quigley@15642
   185
                                   val facthm = read_instantiate [(str1,str2)] th;
quigley@15642
   186
                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
quigley@15642
   187
                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
quigley@15642
   188
                                  val thmvars = thm_vars res'
quigley@15642
   189
                                in 
quigley@15642
   190
                                       (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
quigley@15642
   191
                                end
quigley@15642
   192
                         end;
quigley@15642
   193
quigley@15642
   194
quigley@15642
   195
quigley@15642
   196
Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False";
quigley@15642
   197
val prems = it;
quigley@15642
   198
br (hd prems) 1;
quigley@15642
   199
br (hd(tl(tl prems))) 1;
quigley@15642
   200
qed "merge";
quigley@15642
   201
quigley@15642
   202
quigley@15642
   203
quigley@15642
   204
fun get_unif_comb t eqterm = if ((type_of t ) = (type_of eqterm))
quigley@15642
   205
                             then 
quigley@15642
   206
                                  t
quigley@15642
   207
                             else 
quigley@15642
   208
                                 let val {Rand, Rator} = dest_comb t
quigley@15642
   209
                                 in
quigley@15642
   210
                                     get_unif_comb Rand eqterm
quigley@15642
   211
                                 end
quigley@15642
   212
quigley@15642
   213
fun get_rhs_unif_lit t eqterm = if (can dest_eq t)
quigley@15642
   214
                            then 
quigley@15642
   215
                                let val {lhs, rhs} = dest_eq( t)
quigley@15642
   216
                                in
quigley@15642
   217
                                    rhs
quigley@15642
   218
                                end
quigley@15642
   219
                            else
quigley@15642
   220
                                get_unif_comb t eqterm
quigley@15642
   221
                         
quigley@15642
   222
fun get_lhs_unif_lit t eqterm = if (can dest_eq t)
quigley@15642
   223
                            then 
quigley@15642
   224
                                let val {lhs, rhs} = dest_eq( t)
quigley@15642
   225
                                in
quigley@15642
   226
                                    lhs
quigley@15642
   227
                                end
quigley@15642
   228
                            else
quigley@15642
   229
                                get_unif_comb t eqterm
quigley@15642
   230
quigley@15642
   231
quigley@15642
   232
(*************************************)
quigley@15642
   233
(* Reconstruct a paramodulation step *)
quigley@15642
   234
(*************************************)
quigley@15642
   235
quigley@15642
   236
val rev_subst = rotate_prems 1 subst;
quigley@15642
   237
val rev_ssubst = rotate_prems 1 ssubst;
quigley@15642
   238
quigley@15642
   239
quigley@15642
   240
(* have changed from negate_nead to negate_head.  God knows if this will actually work *)
quigley@15642
   241
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
quigley@15642
   242
                          let 
quigley@15642
   243
                            val th1 =  assoc clause1 thml
quigley@15642
   244
                            val th2 =  assoc clause2 thml 
quigley@15642
   245
                            val eq_lit_th = select_literal (lit1+1) th1
quigley@15642
   246
                            val mod_lit_th = select_literal (lit2+1) th2
quigley@15642
   247
                            val eqsubst = eq_lit_th RSN (2,rev_subst)
quigley@15642
   248
                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
quigley@15642
   249
			    val newth' =negate_head newth 
quigley@15642
   250
                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars 
quigley@15642
   251
                                handle Not_in_list => let 
quigley@15642
   252
                                                  val mod_lit_th' = mod_lit_th RS not_sym
quigley@15642
   253
                                                   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
quigley@15642
   254
			                           val newth' =negate_head newth 
quigley@15642
   255
                                               in 
quigley@15642
   256
                                                  (rearrange_clause newth' clause_strs allvars)
quigley@15642
   257
                                               end)
quigley@15642
   258
                            val thmvars = thm_vars res
quigley@15642
   259
                         in 
quigley@15642
   260
                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
quigley@15642
   261
                         end
quigley@15642
   262
quigley@15642
   263
(*              
quigley@15642
   264
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
quigley@15642
   265
                          let 
quigley@15642
   266
                            val th1 =  assoc clause1 thml
quigley@15642
   267
                            val th2 =  assoc clause2 thml 
quigley@15642
   268
                            val eq_lit_th = select_literal (lit1+1) th1
quigley@15642
   269
                            val mod_lit_th = select_literal (lit2+1) th2
quigley@15642
   270
                            val eqsubst = eq_lit_th RSN (2,rev_subst)
quigley@15642
   271
                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
quigley@15642
   272
			    val newth' =negate_nead newth 
quigley@15642
   273
                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars)
quigley@15642
   274
                            val thmvars = thm_vars res
quigley@15642
   275
                         in 
quigley@15642
   276
                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
quigley@15642
   277
                         end
quigley@15642
   278
quigley@15642
   279
*)
quigley@15642
   280
quigley@15642
   281
quigley@15642
   282
(********************************)
quigley@15642
   283
(* Reconstruct a rewriting step *)
quigley@15642
   284
(********************************)
quigley@15642
   285
 
quigley@15642
   286
(*
quigley@15642
   287
quigley@15642
   288
val rev_subst = rotate_prems 1 subst;
quigley@15642
   289
quigley@15642
   290
fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
quigley@15642
   291
     let  val eq_lit_th = select_literal (lit1+1) cl1
quigley@15642
   292
          val mod_lit_th = select_literal (lit2+1) cl2
quigley@15642
   293
          val eqsubst = eq_lit_th RSN (2,rev_subst)
quigley@15642
   294
          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
quigley@15642
   295
eqsubst)
quigley@15642
   296
     in negated_asm_of_head newth end;
quigley@15642
   297
quigley@15642
   298
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
quigley@15642
   299
eqsubst)
quigley@15642
   300
quigley@15642
   301
val mod_lit_th' = mod_lit_th RS not_sym
quigley@15642
   302
quigley@15642
   303
*)
quigley@15642
   304
quigley@15642
   305
quigley@15642
   306
fun delete_assumps 0 th = th 
quigley@15642
   307
|   delete_assumps n th = let val th_prems = length (prems_of th)
quigley@15642
   308
                              val th' = hd (Seq.list_of(delete_assump_tac  th (th_prems -1)))
quigley@15642
   309
                          in
quigley@15642
   310
                              delete_assumps (n-1) th'
quigley@15642
   311
                          end
quigley@15642
   312
quigley@15642
   313
(* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
quigley@15642
   314
(* changed negate_nead to negate_head here too*)
quigley@15642
   315
                    (* clause1, lit1 is thing to rewrite with *)
quigley@15642
   316
fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= 
quigley@15642
   317
quigley@15642
   318
                          let val th1 =  assoc clause1 thml
quigley@15642
   319
                              val th2 = assoc clause2 thml
quigley@15642
   320
                              val eq_lit_th = select_literal (lit1+1) th1
quigley@15642
   321
                              val mod_lit_th = select_literal (lit2+1) th2
quigley@15642
   322
                              val eqsubst = eq_lit_th RSN (2,rev_subst)
quigley@15642
   323
                              val eq_lit_prem_num = length (prems_of eq_lit_th)
quigley@15642
   324
                              val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
quigley@15642
   325
                              val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
quigley@15642
   326
eqsubst)
quigley@15642
   327
                         
quigley@15642
   328
                              val newthm = negate_head newth
quigley@15642
   329
                              val newthm' = delete_assumps eq_lit_prem_num newthm
quigley@15642
   330
                              val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
quigley@15642
   331
                              val thmvars = thm_vars res
quigley@15642
   332
                           in
quigley@15642
   333
                               (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
quigley@15642
   334
                           end
quigley@15642
   335
quigley@15642
   336
quigley@15642
   337
quigley@15642
   338
(*****************************************)
quigley@15642
   339
(* Reconstruct an obvious reduction step *)
quigley@15642
   340
(*****************************************)
quigley@15642
   341
quigley@15642
   342
quigley@15642
   343
fun follow_obvious  (clause1, lit1)  allvars thml clause_strs= 
quigley@15642
   344
                           let val th1 =  assoc clause1 thml
quigley@15642
   345
                               val prems1 = prems_of th1
quigley@15642
   346
                               val newthm = refl RSN ((lit1+ 1), th1)
quigley@15642
   347
                                               handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
quigley@15642
   348
                               val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
quigley@15642
   349
                               val thmvars = thm_vars res
quigley@15642
   350
                           in 
quigley@15642
   351
                               (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
quigley@15642
   352
                           end
quigley@15642
   353
quigley@15642
   354
(**************************************************************************************)
quigley@15642
   355
(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
quigley@15642
   356
(**************************************************************************************)
quigley@15642
   357
quigley@15642
   358
 fun follow_proof clauses allvars  clausenum thml  (Axiom ) clause_strs
quigley@15642
   359
        = follow_axiom clauses allvars  clausenum thml clause_strs
quigley@15642
   360
quigley@15642
   361
      | follow_proof clauses  allvars clausenum  thml (Binary (a, b)) clause_strs
quigley@15642
   362
        = follow_binary  (a, b)  allvars thml clause_strs
quigley@15642
   363
quigley@15642
   364
      | follow_proof clauses  allvars clausenum  thml (MRR (a, b)) clause_strs
quigley@15642
   365
        = follow_mrr (a, b)  allvars thml clause_strs
quigley@15642
   366
quigley@15642
   367
      | follow_proof clauses  allvars clausenum  thml (Factor (a, b, c)) clause_strs
quigley@15642
   368
         = follow_factor a b c  allvars thml clause_strs
quigley@15642
   369
quigley@15642
   370
      | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
quigley@15642
   371
        = follow_standard_para (a, b) allvars  thml clause_strs
quigley@15642
   372
quigley@15642
   373
      | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
quigley@15642
   374
        = follow_rewrite (a,b)  allvars thml clause_strs
quigley@15642
   375
quigley@15642
   376
      | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
quigley@15642
   377
        = follow_obvious (a,b)  allvars thml clause_strs
quigley@15642
   378
quigley@15642
   379
      (*| follow_proof clauses  clausenum thml (Hyper l)
quigley@15642
   380
        = follow_hyper l thml*)
quigley@15642
   381
      | follow_proof clauses  allvars clausenum  thml _ _ =
quigley@15642
   382
          raise ASSERTION  "proof step not implemented"
quigley@15642
   383
quigley@15642
   384
quigley@15642
   385
quigley@15642
   386
 
quigley@15642
   387
(**************************************************************************************)
quigley@15642
   388
(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
quigley@15642
   389
(**************************************************************************************)
quigley@15642
   390
quigley@15642
   391
    fun follow_line clauses  allvars thml (clause_num, proof_step, clause_strs) recons
quigley@15642
   392
        = let
quigley@15642
   393
            val (thm, recon_fun) = follow_proof clauses  allvars clause_num thml proof_step clause_strs 
quigley@15642
   394
            val recon_step = (recon_fun)
quigley@15642
   395
          in
quigley@15642
   396
            (((clause_num, thm)::thml), ((clause_num,recon_step)::recons))
quigley@15642
   397
          end
quigley@15642
   398
quigley@15642
   399
(***************************************************************)
quigley@15642
   400
(* follow through the res. proof, creating an Isabelle theorem *)
quigley@15642
   401
(***************************************************************)
quigley@15642
   402
quigley@15642
   403
quigley@15642
   404
quigley@15642
   405
(*fun is_proof_char ch = (case ch of 
quigley@15642
   406
                       
quigley@15642
   407
                        "(" => true
quigley@15642
   408
                       |  ")" => true
quigley@15642
   409
                         | ":" => true
quigley@15642
   410
                        |  "'" => true
quigley@15642
   411
                        |  "&" => true
quigley@15642
   412
                        | "|" => true
quigley@15642
   413
                        | "~" => true
quigley@15642
   414
                        |  "." => true
quigley@15642
   415
                        |(is_alpha ) => true
quigley@15642
   416
                       |(is_digit) => true
quigley@15642
   417
                         | _ => false)*)
quigley@15642
   418
quigley@15642
   419
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
quigley@15642
   420
quigley@15642
   421
fun proofstring x = let val exp = explode x 
quigley@15642
   422
                    in
quigley@15642
   423
                        List.filter (is_proof_char ) exp
quigley@15642
   424
                    end
quigley@15642
   425
quigley@15642
   426
quigley@15642
   427
fun not_newline ch = not (ch = "\n");
quigley@15642
   428
quigley@15642
   429
fun concat_with_and [] str = str
quigley@15642
   430
|   concat_with_and (x::[]) str = str^"("^x^")"
quigley@15642
   431
|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
quigley@15642
   432
(*
quigley@15642
   433
quigley@15642
   434
fun follow clauses [] allvars thml recons = 
quigley@15642
   435
                             let (* val _ = reset show_sorts*)
quigley@15642
   436
                              val thmstring = concat_with_and (map string_of_thm (map snd thml)) ""
quigley@15642
   437
                              val thmproofstring = proofstring ( thmstring)
quigley@15642
   438
                            val no_returns =List.filter  not_newline ( thmproofstring)
quigley@15642
   439
                            val thmstr = implode no_returns
quigley@15658
   440
                               val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
quigley@15642
   441
                               val _ = TextIO.output(outfile, "thmstr is "^thmstr)
quigley@15642
   442
                               val _ = TextIO.flushOut outfile;
quigley@15642
   443
                               val _ =  TextIO.closeOut outfile
quigley@15642
   444
                                 (*val _ = set show_sorts*)
quigley@15642
   445
                             in
quigley@15642
   446
                                  ((snd( hd thml)), recons)
quigley@15642
   447
                             end
quigley@15642
   448
      | follow clauses (h::t) allvars thml recons 
quigley@15642
   449
        = let
quigley@15642
   450
            val (thml', recons') = follow_line clauses allvars  thml h recons
quigley@15642
   451
            val  (thm, recons_list) = follow clauses t  allvars thml' recons'
quigley@15642
   452
            
quigley@15642
   453
quigley@15642
   454
          in
quigley@15642
   455
             (thm,recons_list)
quigley@15642
   456
          end
quigley@15642
   457
quigley@15642
   458
*)
quigley@15642
   459
quigley@15642
   460
fun replace_clause_strs [] recons newrecons= (newrecons)
quigley@15642
   461
|   replace_clause_strs ((thmnum, thm)::thml)  ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
quigley@15642
   462
                           let val new_clause_strs = get_meta_lits_bracket thm
quigley@15642
   463
                           in
quigley@15642
   464
                               replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
quigley@15642
   465
                           end
quigley@15642
   466
quigley@15642
   467
quigley@15642
   468
fun follow clauses [] allvars thml recons = 
quigley@15642
   469
                             let 
quigley@15642
   470
                                 val new_recons = replace_clause_strs thml recons []
quigley@15642
   471
                             in
quigley@15642
   472
                                  ((snd( hd thml)), new_recons)
quigley@15642
   473
                             end
quigley@15642
   474
quigley@15642
   475
 |  follow clauses (h::t) allvars thml recons 
quigley@15642
   476
        = let
quigley@15642
   477
            val (thml', recons') = follow_line clauses allvars  thml h recons
quigley@15642
   478
            val  (thm, recons_list) = follow clauses t  allvars thml' recons'     
quigley@15642
   479
          in
quigley@15642
   480
             (thm,recons_list)
quigley@15642
   481
          end
quigley@15642
   482
quigley@15642
   483
quigley@15642
   484
quigley@15642
   485
(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
quigley@15642
   486
 (* and the proof as a list of the proper datatype *)
quigley@15642
   487
(* take the cnf clauses of the goal and the proof from the res. prover *)
quigley@15642
   488
(* as a list of type Proofstep and return the thm goal ==> False *)
quigley@15642
   489
quigley@15642
   490
fun first_pair (a,b,c) = (a,b);
quigley@15642
   491
quigley@15642
   492
fun second_pair (a,b,c) = (b,c);
quigley@15642
   493
quigley@15642
   494
fun one_of_three (a,b,c) = a;
quigley@15642
   495
fun two_of_three (a,b,c) = b;
quigley@15642
   496
fun three_of_three (a,b,c) = c;
quigley@15642
   497
quigley@15642
   498
quigley@15642
   499
(* takes original axioms, proof_steps parsed from spass, variables *)
quigley@15642
   500
quigley@15642
   501
fun translate_proof clauses proof allvars
quigley@15642
   502
        = let val (thm, recons) = follow clauses proof allvars [] []
quigley@15642
   503
          in
quigley@15642
   504
             (thm, (recons))
quigley@15642
   505
          end
quigley@15642
   506
  
quigley@15642
   507
quigley@15642
   508
quigley@15642
   509
fun remove_tinfo [] = []
quigley@15642
   510
|   remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs)