src/HOL/Tools/ATP/recon_translate_proof.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 17776 4a518eec4a20
child 19643 213e12ad2c03
permissions -rw-r--r--
improved code generator devarification
paulson@15789
     1
(*  ID:         $Id$
paulson@15789
     2
    Author:     Claire Quigley
paulson@15789
     3
    Copyright   2004  University of Cambridge
paulson@15789
     4
*)
quigley@15642
     5
wenzelm@16803
     6
structure ReconTranslateProof =
wenzelm@16803
     7
struct
wenzelm@16803
     8
quigley@15642
     9
fun add_in_order (x:string) [] = [x]
quigley@15642
    10
|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
quigley@15642
    11
                             then 
quigley@15642
    12
                                  (x::(y::ys))
quigley@15642
    13
                             else
quigley@15642
    14
                                  (y::(add_in_order x ys))
quigley@15642
    15
fun add_once x [] = [x]
paulson@16157
    16
|   add_once x (y::ys) = if x mem (y::ys) then (y::ys)
paulson@16157
    17
                         else add_in_order x (y::ys)
quigley@15642
    18
     
paulson@15684
    19
fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
quigley@15642
    20
quigley@15642
    21
exception Reflex_equal;
quigley@15642
    22
quigley@15642
    23
(********************************)
quigley@15642
    24
(* Proofstep datatype           *)
quigley@15642
    25
(********************************)
quigley@15642
    26
(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)
quigley@15642
    27
quigley@15642
    28
datatype Side = Left |Right
quigley@15642
    29
wenzelm@16803
    30
datatype Proofstep =  ExtraAxiom
quigley@16418
    31
                     | OrigAxiom
quigley@16418
    32
  		     | VampInput 
quigley@15642
    33
                     | Axiom
quigley@15642
    34
                     | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
quigley@15642
    35
                     | MRR of (int * int) * (int * int) 
quigley@15642
    36
                     | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
quigley@15642
    37
                     | Para of (int * int) * (int * int) 
quigley@16357
    38
		     | Super_l of (int * int) * (int * int)
quigley@16357
    39
		     | Super_r of (int * int) * (int * int)
quigley@16548
    40
                     (*| Rewrite of (int * int) * (int * int)  *)
quigley@16548
    41
                     | Rewrite of (int * int) list
quigley@16357
    42
		     | SortSimp of (int * int) * (int * int)  
quigley@16357
    43
		     | UnitConf of (int * int) * (int * int)  
quigley@15642
    44
                     | Obvious of (int * int)
quigley@16357
    45
  		     | AED of (int*int)
quigley@16357
    46
  		     | EqualRes of (int*int)
quigley@16357
    47
    		     | Condense of (int*int)
quigley@15642
    48
                     (*| Hyper of int list*)
quigley@15642
    49
                     | Unusedstep of unit
quigley@15642
    50
quigley@15642
    51
quigley@15642
    52
datatype Clausesimp = Binary_s of int * int
quigley@15642
    53
                      | Factor_s of unit
quigley@15642
    54
                      | Demod_s of (int * int) list
quigley@15642
    55
                      | Hyper_s of int list
quigley@15642
    56
                      | Unusedstep_s of unit
quigley@15642
    57
quigley@15642
    58
quigley@15642
    59
quigley@15642
    60
datatype Step_label = T_info
quigley@15642
    61
                     |P_info
quigley@15642
    62
quigley@15642
    63
paulson@16061
    64
fun is_alpha_space_digit_or_neg ch =
paulson@16061
    65
    (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse 
paulson@16061
    66
    (ReconOrderClauses.is_digit ch) orelse ( ch = " ");
quigley@15642
    67
wenzelm@17776
    68
fun lit_string_with_nums t = let val termstr = Term.str_of_term t
quigley@15642
    69
                                 val exp_term = explode termstr
quigley@15642
    70
                             in
quigley@15642
    71
                                 implode(List.filter is_alpha_space_digit_or_neg exp_term)
quigley@15642
    72
                             end
quigley@15642
    73
paulson@15774
    74
fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
quigley@15642
    75
quigley@15919
    76
(************************************************)
quigley@15919
    77
(* Reconstruct an axiom resolution step         *)
quigley@15919
    78
(* clauses is a list of (clausenum,clause) pairs*)
quigley@15919
    79
(************************************************)
quigley@15642
    80
paulson@15774
    81
fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
haftmann@17374
    82
    let val this_axiom = (the o AList.lookup (op =) clauses) clausenum
paulson@16061
    83
	val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)         
paulson@16061
    84
	val thmvars = thm_vars res
paulson@16061
    85
    in
paulson@16061
    86
	(res, (Axiom,clause_strs,thmvars )  )
paulson@16061
    87
    end
paulson@16061
    88
    handle Option => reconstruction_failed "follow_axiom"
quigley@15642
    89
quigley@15642
    90
(****************************************)
quigley@15642
    91
(* Reconstruct a binary resolution step *)
quigley@15642
    92
(****************************************)
quigley@15642
    93
quigley@15642
    94
                 (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
paulson@16061
    95
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
haftmann@17374
    96
    let val thm1 =  select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
haftmann@17374
    97
	val thm2 =  (the o AList.lookup (op =) thml) clause2
paulson@16061
    98
	val res =   thm1 RSN ((lit2 +1), thm2)
paulson@16061
    99
	val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
paulson@16061
   100
	val thmvars = thm_vars res
paulson@16061
   101
    in
paulson@16061
   102
       (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
paulson@16061
   103
    end
paulson@16061
   104
    handle Option => reconstruction_failed "follow_binary"
quigley@15642
   105
quigley@15642
   106
quigley@15642
   107
quigley@15642
   108
(******************************************************)
quigley@15642
   109
(* Reconstruct a matching replacement resolution step *)
quigley@15642
   110
(******************************************************)
quigley@15642
   111
quigley@15642
   112
paulson@16061
   113
fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs =
haftmann@17374
   114
    let val thm1 =  select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
haftmann@17374
   115
	val thm2 =  (the o AList.lookup (op =) thml) clause2
paulson@16061
   116
	val res =   thm1 RSN ((lit2 +1), thm2)
paulson@16061
   117
	val (res', numlist, symlist, nsymlist) = 
paulson@16061
   118
	    (ReconOrderClauses.rearrange_clause res clause_strs allvars)
paulson@16061
   119
	val thmvars = thm_vars res
paulson@16061
   120
    in
paulson@16061
   121
       (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
paulson@16061
   122
    end
paulson@16061
   123
    handle Option => reconstruction_failed "follow_mrr"
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
paulson@16061
   131
   |mksubstlist ((a, (_, b)) :: rest) sublist = 
paulson@16061
   132
       let val vartype = type_of b 
paulson@16061
   133
	   val avar = Var(a,vartype)
paulson@16061
   134
	   val newlist = ((avar,b)::sublist)
paulson@16061
   135
       in
paulson@16061
   136
	   mksubstlist rest newlist
paulson@16061
   137
       end;
quigley@15642
   138
quigley@15642
   139
(* based on Tactic.distinct_subgoals_tac *)
quigley@15642
   140
quigley@15642
   141
fun delete_assump_tac state lit =
quigley@15642
   142
    let val (frozth,thawfn) = freeze_thaw state
quigley@15642
   143
        val froz_prems = cprems_of frozth
quigley@15642
   144
        val assumed = implies_elim_list frozth (map assume froz_prems)
paulson@16061
   145
        val new_prems = ReconOrderClauses.remove_nth lit froz_prems
quigley@15642
   146
        val implied = implies_intr_list new_prems assumed
quigley@15642
   147
    in  
quigley@15642
   148
        Seq.single (thawfn implied)  
quigley@15642
   149
    end
quigley@15642
   150
quigley@15642
   151
quigley@15642
   152
quigley@15642
   153
quigley@15642
   154
quigley@15642
   155
(*************************************)
quigley@15642
   156
(* Reconstruct a factoring step      *)
quigley@15642
   157
(*************************************)
quigley@15642
   158
paulson@17488
   159
fun getnewenv seq = fst (fst (the (Seq.pull seq)));
paulson@17488
   160
paulson@15739
   161
(*FIXME: share code with that in Tools/reconstruction.ML*)
paulson@16061
   162
fun follow_factor clause lit1 lit2 allvars thml clause_strs = 
paulson@16061
   163
    let 
haftmann@17374
   164
      val th =  (the o AList.lookup (op =) thml) clause
paulson@16061
   165
      val prems = prems_of th
paulson@16061
   166
      val sign = sign_of_thm th
paulson@16061
   167
      val fac1 = ReconOrderClauses.get_nth (lit1+1) prems
paulson@16061
   168
      val fac2 = ReconOrderClauses.get_nth (lit2+1) prems
paulson@16061
   169
      val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
paulson@16061
   170
      val newenv = getnewenv unif_env
paulson@16061
   171
      val envlist = Envir.alist_of newenv
paulson@16061
   172
      
paulson@16061
   173
      val (t1,t2)::_ = mksubstlist envlist []
paulson@16061
   174
    in 
paulson@16061
   175
      if (is_Var t1)
paulson@16061
   176
      then
paulson@16061
   177
	  let 
paulson@16061
   178
	     val str1 = lit_string_with_nums t1;
paulson@16061
   179
	     val str2 = lit_string_with_nums t2;
paulson@16061
   180
	     val facthm = read_instantiate [(str1,str2)] th;
paulson@16061
   181
	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
paulson@16061
   182
	     val (res', numlist, symlist, nsymlist) = 
paulson@16061
   183
	         ReconOrderClauses.rearrange_clause res clause_strs allvars
paulson@16061
   184
	     val thmvars = thm_vars res'
paulson@16061
   185
	  in 
paulson@16061
   186
		 (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
paulson@16061
   187
	  end
paulson@16061
   188
      else
paulson@16061
   189
	  let
paulson@16061
   190
	     val str2 = lit_string_with_nums t1;
paulson@16061
   191
	     val str1 = lit_string_with_nums t2;
paulson@16061
   192
	     val facthm = read_instantiate [(str1,str2)] th;
paulson@16061
   193
	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
paulson@16061
   194
	     val (res', numlist, symlist, nsymlist) = 
paulson@16061
   195
	         ReconOrderClauses.rearrange_clause res clause_strs allvars
paulson@16061
   196
	     val thmvars = thm_vars res'
paulson@16061
   197
	  in 
paulson@16061
   198
		 (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
paulson@16061
   199
	  end
paulson@16061
   200
   end
paulson@16061
   201
   handle Option => reconstruction_failed "follow_factor"
quigley@15642
   202
quigley@15642
   203
quigley@15642
   204
paulson@15684
   205
fun get_unif_comb t eqterm =
paulson@15684
   206
    if ((type_of t) = (type_of eqterm))
paulson@15684
   207
    then t
paulson@15684
   208
    else
paulson@15684
   209
        let val _ $ rand = t
paulson@15684
   210
        in get_unif_comb rand eqterm end;
quigley@15642
   211
paulson@15684
   212
fun get_unif_lit t eqterm =
paulson@15684
   213
    if (can HOLogic.dest_eq t)
paulson@15684
   214
    then
paulson@15684
   215
	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
paulson@15684
   216
	in lhs end
paulson@15684
   217
    else
paulson@15684
   218
	get_unif_comb t eqterm;
paulson@15684
   219
quigley@15642
   220
quigley@15642
   221
quigley@15642
   222
(*************************************)
quigley@15642
   223
(* Reconstruct a paramodulation step *)
quigley@15642
   224
(*************************************)
quigley@15642
   225
quigley@15642
   226
val rev_subst = rotate_prems 1 subst;
quigley@15642
   227
val rev_ssubst = rotate_prems 1 ssubst;
quigley@15642
   228
quigley@15642
   229
paulson@16061
   230
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = 
paulson@16061
   231
    let 
haftmann@17374
   232
      val th1 =  (the o AList.lookup (op =) thml) clause1
haftmann@17374
   233
      val th2 =  (the o AList.lookup (op =) thml) clause2 
paulson@16061
   234
      val eq_lit_th = select_literal (lit1+1) th1
paulson@16061
   235
      val mod_lit_th = select_literal (lit2+1) th2
paulson@16061
   236
      val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@16061
   237
      val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
paulson@16061
   238
      val newth' =negate_head newth 
paulson@16061
   239
      val (res, numlist, symlist, nsymlist)  = 
paulson@16061
   240
          (ReconOrderClauses.rearrange_clause newth' clause_strs allvars 
paulson@16061
   241
	   handle Not_in_list => 
paulson@16061
   242
	       let val mod_lit_th' = mod_lit_th RS not_sym
paulson@16061
   243
		   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
paulson@16061
   244
		   val newth' =negate_head newth 
paulson@16061
   245
		in 
paulson@16061
   246
		   ReconOrderClauses.rearrange_clause newth' clause_strs allvars
paulson@16061
   247
		end)
paulson@16061
   248
      val thmvars = thm_vars res
paulson@16061
   249
   in 
paulson@16061
   250
     (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
paulson@16061
   251
   end
paulson@16061
   252
   handle Option => reconstruction_failed "follow_standard_para"
quigley@15642
   253
quigley@15642
   254
quigley@15642
   255
(********************************)
quigley@15642
   256
(* Reconstruct a rewriting step *)
quigley@15642
   257
(********************************)
quigley@15642
   258
 
quigley@15642
   259
(*
quigley@15642
   260
quigley@15642
   261
val rev_subst = rotate_prems 1 subst;
quigley@15642
   262
quigley@15642
   263
fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
quigley@15642
   264
     let  val eq_lit_th = select_literal (lit1+1) cl1
quigley@15642
   265
          val mod_lit_th = select_literal (lit2+1) cl2
quigley@15642
   266
          val eqsubst = eq_lit_th RSN (2,rev_subst)
quigley@15642
   267
          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
quigley@15642
   268
eqsubst)
paulson@15697
   269
     in Meson.negated_asm_of_head newth end;
quigley@15642
   270
quigley@15642
   271
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
quigley@15642
   272
eqsubst)
quigley@15642
   273
quigley@15642
   274
val mod_lit_th' = mod_lit_th RS not_sym
quigley@15642
   275
quigley@15642
   276
*)
quigley@15642
   277
quigley@15642
   278
quigley@15642
   279
fun delete_assumps 0 th = th 
quigley@15642
   280
|   delete_assumps n th = let val th_prems = length (prems_of th)
quigley@15642
   281
                              val th' = hd (Seq.list_of(delete_assump_tac  th (th_prems -1)))
quigley@15642
   282
                          in
quigley@15642
   283
                              delete_assumps (n-1) th'
quigley@15642
   284
                          end
quigley@15642
   285
quigley@15642
   286
(* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
quigley@15642
   287
(* changed negate_nead to negate_head here too*)
quigley@15642
   288
                    (* clause1, lit1 is thing to rewrite with *)
quigley@16548
   289
(*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = 
haftmann@17374
   290
      let val th1 =  (the o AList.lookup (op =) thml) clause1
haftmann@17374
   291
	  val th2 = (the o AList.lookup (op =) thml) clause2
paulson@16061
   292
	  val eq_lit_th = select_literal (lit1+1) th1
paulson@16061
   293
	  val mod_lit_th = select_literal (lit2+1) th2
paulson@16061
   294
	  val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@16061
   295
	  val eq_lit_prem_num = length (prems_of eq_lit_th)
wenzelm@16433
   296
	  val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2)
paulson@16061
   297
	  val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
paulson@16061
   298
     	  val newthm = negate_head newth
paulson@16061
   299
	  val newthm' = delete_assumps eq_lit_prem_num newthm
paulson@16061
   300
	  val (res, numlist, symlist, nsymlist) =
paulson@16061
   301
	      ReconOrderClauses.rearrange_clause newthm clause_strs allvars
paulson@16061
   302
	  val thmvars = thm_vars res
paulson@16061
   303
       in
paulson@16061
   304
	   (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
paulson@16061
   305
       end
paulson@16061
   306
       handle Option => reconstruction_failed "follow_rewrite"
quigley@15642
   307
quigley@16548
   308
*)
quigley@15642
   309
quigley@15642
   310
(*****************************************)
quigley@15642
   311
(* Reconstruct an obvious reduction step *)
quigley@15642
   312
(*****************************************)
quigley@15642
   313
quigley@15642
   314
paulson@16061
   315
fun follow_obvious  (clause1, lit1)  allvars thml clause_strs = 
haftmann@17374
   316
    let val th1 =  (the o AList.lookup (op =) thml) clause1
paulson@16061
   317
	val prems1 = prems_of th1
paulson@16061
   318
	val newthm = refl RSN ((lit1+ 1), th1)
paulson@16061
   319
		     handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
paulson@16061
   320
	val (res, numlist, symlist, nsymlist) =
paulson@16061
   321
	    ReconOrderClauses.rearrange_clause newthm clause_strs allvars
paulson@16061
   322
	val thmvars = thm_vars res
paulson@16061
   323
    in 
paulson@16061
   324
	(res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
paulson@16061
   325
    end
paulson@16061
   326
    handle Option => reconstruction_failed "follow_obvious"
quigley@15642
   327
quigley@15642
   328
(**************************************************************************************)
quigley@15642
   329
(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
quigley@15642
   330
(**************************************************************************************)
quigley@15642
   331
quigley@15642
   332
 fun follow_proof clauses allvars  clausenum thml  (Axiom ) clause_strs
quigley@15642
   333
        = follow_axiom clauses allvars  clausenum thml clause_strs
quigley@15642
   334
quigley@15642
   335
      | follow_proof clauses  allvars clausenum  thml (Binary (a, b)) clause_strs
quigley@15642
   336
        = follow_binary  (a, b)  allvars thml clause_strs
quigley@15642
   337
quigley@15642
   338
      | follow_proof clauses  allvars clausenum  thml (MRR (a, b)) clause_strs
quigley@15642
   339
        = follow_mrr (a, b)  allvars thml clause_strs
quigley@15642
   340
quigley@15642
   341
      | follow_proof clauses  allvars clausenum  thml (Factor (a, b, c)) clause_strs
quigley@15642
   342
         = follow_factor a b c  allvars thml clause_strs
quigley@15642
   343
quigley@15642
   344
      | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
quigley@15642
   345
        = follow_standard_para (a, b) allvars  thml clause_strs
quigley@15642
   346
quigley@16548
   347
    (*  | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
quigley@16548
   348
        = follow_rewrite (a,b)  allvars thml clause_strs*)
quigley@15642
   349
quigley@15642
   350
      | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
quigley@15642
   351
        = follow_obvious (a,b)  allvars thml clause_strs
quigley@15642
   352
quigley@15642
   353
      (*| follow_proof clauses  clausenum thml (Hyper l)
quigley@15642
   354
        = follow_hyper l thml*)
quigley@15642
   355
      | follow_proof clauses  allvars clausenum  thml _ _ =
paulson@17488
   356
          error "proof step not implemented"
quigley@15642
   357
quigley@15642
   358
quigley@15642
   359
quigley@15642
   360
 
quigley@15642
   361
(**************************************************************************************)
quigley@15642
   362
(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
quigley@15642
   363
(**************************************************************************************)
quigley@15642
   364
paulson@17488
   365
    fun follow_line clauses  allvars thml (clause_num, proof_step, clause_strs) recons =
paulson@17488
   366
      let
paulson@17488
   367
	val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs 
paulson@17488
   368
      in
paulson@17488
   369
	((clause_num, thm)::thml, (clause_num,recon_fun)::recons)
paulson@17488
   370
      end
quigley@15642
   371
quigley@15642
   372
(***************************************************************)
quigley@15642
   373
(* follow through the res. proof, creating an Isabelle theorem *)
quigley@15642
   374
(***************************************************************)
quigley@15642
   375
quigley@15642
   376
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
quigley@15642
   377
quigley@15642
   378
fun proofstring x = let val exp = explode x 
quigley@15642
   379
                    in
quigley@15642
   380
                        List.filter (is_proof_char ) exp
quigley@15642
   381
                    end
quigley@15642
   382
paulson@16061
   383
fun replace_clause_strs [] recons newrecons = (newrecons)
paulson@16061
   384
|   replace_clause_strs ((thmnum, thm)::thml)    
paulson@16061
   385
                  ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
paulson@16061
   386
    let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm
paulson@16061
   387
    in
paulson@16061
   388
	replace_clause_strs thml recons  
paulson@16061
   389
	    ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
paulson@16061
   390
    end
quigley@15642
   391
quigley@15642
   392
quigley@15642
   393
fun follow clauses [] allvars thml recons = 
paulson@16061
   394
      let 
paulson@16061
   395
	  val new_recons = replace_clause_strs thml recons []
paulson@16061
   396
      in
paulson@16061
   397
	   (#2(hd thml), new_recons)
paulson@16061
   398
      end
paulson@16061
   399
 | follow clauses (h::t) allvars thml recons =
paulson@16061
   400
      let
paulson@16061
   401
	val (thml', recons') = follow_line clauses allvars  thml h recons
paulson@16061
   402
	val  (thm, recons_list) = follow clauses t  allvars thml' recons'     
paulson@16061
   403
      in
paulson@16061
   404
	 (thm,recons_list)
paulson@16061
   405
      end
quigley@15642
   406
quigley@15642
   407
(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
quigley@15642
   408
 (* and the proof as a list of the proper datatype *)
quigley@15642
   409
(* take the cnf clauses of the goal and the proof from the res. prover *)
quigley@15642
   410
(* as a list of type Proofstep and return the thm goal ==> False *)
quigley@15642
   411
quigley@15642
   412
(* takes original axioms, proof_steps parsed from spass, variables *)
quigley@15642
   413
quigley@15642
   414
fun translate_proof clauses proof allvars
quigley@15642
   415
        = let val (thm, recons) = follow clauses proof allvars [] []
quigley@15642
   416
          in
quigley@15642
   417
             (thm, (recons))
quigley@15642
   418
          end
quigley@15642
   419
  
wenzelm@16803
   420
end;