src/HOL/Tools/ATP/recon_translate_proof.ML
author quigley
Wed Jun 22 20:26:31 2005 +0200 (2005-06-22)
changeset 16548 aa36ae6b955e
parent 16433 e6fedd5baf32
child 16707 c28599f981f2
permissions -rw-r--r--
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.
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
quigley@15642
     6
fun add_in_order (x:string) [] = [x]
quigley@15642
     7
|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
quigley@15642
     8
                             then 
quigley@15642
     9
                                  (x::(y::ys))
quigley@15642
    10
                             else
quigley@15642
    11
                                  (y::(add_in_order x ys))
quigley@15642
    12
fun add_once x [] = [x]
paulson@16157
    13
|   add_once x (y::ys) = if x mem (y::ys) then (y::ys)
paulson@16157
    14
                         else add_in_order x (y::ys)
quigley@15642
    15
     
paulson@15684
    16
fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
quigley@15642
    17
quigley@15642
    18
Goal "False ==> False";
quigley@15642
    19
by Auto_tac;
quigley@15642
    20
qed "False_imp";
quigley@15642
    21
quigley@15642
    22
exception Reflex_equal;
quigley@15642
    23
quigley@15642
    24
(********************************)
quigley@15642
    25
(* Proofstep datatype           *)
quigley@15642
    26
(********************************)
quigley@15642
    27
(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3]  *)
quigley@15642
    28
quigley@15642
    29
datatype Side = Left |Right
quigley@15642
    30
quigley@16418
    31
 datatype Proofstep =  ExtraAxiom
quigley@16418
    32
                     | OrigAxiom
quigley@16418
    33
  		     | VampInput 
quigley@15642
    34
                     | Axiom
quigley@15642
    35
                     | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
quigley@15642
    36
                     | MRR of (int * int) * (int * int) 
quigley@15642
    37
                     | Factor of (int * int * int)           (* (clause,lit1, lit2) *)
quigley@15642
    38
                     | Para of (int * int) * (int * int) 
quigley@16357
    39
		     | Super_l of (int * int) * (int * int)
quigley@16357
    40
		     | Super_r of (int * int) * (int * int)
quigley@16548
    41
                     (*| Rewrite of (int * int) * (int * int)  *)
quigley@16548
    42
                     | Rewrite of (int * int) list
quigley@16357
    43
		     | SortSimp of (int * int) * (int * int)  
quigley@16357
    44
		     | UnitConf of (int * int) * (int * int)  
quigley@15642
    45
                     | Obvious of (int * int)
quigley@16357
    46
  		     | AED of (int*int)
quigley@16357
    47
  		     | EqualRes of (int*int)
quigley@16357
    48
    		     | Condense of (int*int)
quigley@15642
    49
                     (*| Hyper of int list*)
quigley@15642
    50
                     | Unusedstep of unit
quigley@15642
    51
quigley@15642
    52
quigley@15642
    53
datatype Clausesimp = Binary_s of int * int
quigley@15642
    54
                      | Factor_s of unit
quigley@15642
    55
                      | Demod_s of (int * int) list
quigley@15642
    56
                      | Hyper_s of int list
quigley@15642
    57
                      | Unusedstep_s of unit
quigley@15642
    58
quigley@15642
    59
quigley@15642
    60
quigley@15642
    61
datatype Step_label = T_info
quigley@15642
    62
                     |P_info
quigley@15642
    63
quigley@15642
    64
paulson@16061
    65
fun is_alpha_space_digit_or_neg ch =
paulson@16061
    66
    (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse 
paulson@16061
    67
    (ReconOrderClauses.is_digit ch) orelse ( ch = " ");
quigley@15642
    68
quigley@15642
    69
paulson@15697
    70
fun lit_string_with_nums t = let val termstr = Term.string_of_term t
quigley@15642
    71
                                 val exp_term = explode termstr
quigley@15642
    72
                             in
quigley@15642
    73
                                 implode(List.filter is_alpha_space_digit_or_neg exp_term)
quigley@15642
    74
                             end
quigley@15642
    75
paulson@15774
    76
fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
quigley@15642
    77
quigley@15919
    78
(************************************************)
quigley@15919
    79
(* Reconstruct an axiom resolution step         *)
quigley@15919
    80
(* clauses is a list of (clausenum,clause) pairs*)
quigley@15919
    81
(************************************************)
quigley@15642
    82
paulson@15774
    83
fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
paulson@16061
    84
    let val this_axiom = valOf (assoc (clauses,clausenum))
paulson@16061
    85
	val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)         
paulson@16061
    86
	val thmvars = thm_vars res
paulson@16061
    87
    in
paulson@16061
    88
	(res, (Axiom,clause_strs,thmvars )  )
paulson@16061
    89
    end
paulson@16061
    90
    handle Option => reconstruction_failed "follow_axiom"
quigley@15642
    91
quigley@15642
    92
(****************************************)
quigley@15642
    93
(* Reconstruct a binary resolution step *)
quigley@15642
    94
(****************************************)
quigley@15642
    95
quigley@15642
    96
                 (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
paulson@16061
    97
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
paulson@16061
    98
    let val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
paulson@16061
    99
	val thm2 =  valOf (assoc (thml,clause2))
paulson@16061
   100
	val res =   thm1 RSN ((lit2 +1), thm2)
paulson@16061
   101
	val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
paulson@16061
   102
	val thmvars = thm_vars res
paulson@16061
   103
    in
paulson@16061
   104
       (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
paulson@16061
   105
    end
paulson@16061
   106
    handle Option => reconstruction_failed "follow_binary"
quigley@15642
   107
quigley@15642
   108
quigley@15642
   109
quigley@15642
   110
(******************************************************)
quigley@15642
   111
(* Reconstruct a matching replacement resolution step *)
quigley@15642
   112
(******************************************************)
quigley@15642
   113
quigley@15642
   114
paulson@16061
   115
fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs =
paulson@16061
   116
    let val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
paulson@16061
   117
	val thm2 =  valOf (assoc (thml,clause2))
paulson@16061
   118
	val res =   thm1 RSN ((lit2 +1), thm2)
paulson@16061
   119
	val (res', numlist, symlist, nsymlist) = 
paulson@16061
   120
	    (ReconOrderClauses.rearrange_clause res clause_strs allvars)
paulson@16061
   121
	val thmvars = thm_vars res
paulson@16061
   122
    in
paulson@16061
   123
       (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
paulson@16061
   124
    end
paulson@16061
   125
    handle Option => reconstruction_failed "follow_mrr"
quigley@15642
   126
quigley@15642
   127
quigley@15642
   128
(*******************************************)
quigley@15642
   129
(* Reconstruct a factoring resolution step *)
quigley@15642
   130
(*******************************************)
quigley@15642
   131
quigley@15642
   132
fun mksubstlist [] sublist = sublist
paulson@16061
   133
   |mksubstlist ((a, (_, b)) :: rest) sublist = 
paulson@16061
   134
       let val vartype = type_of b 
paulson@16061
   135
	   val avar = Var(a,vartype)
paulson@16061
   136
	   val newlist = ((avar,b)::sublist)
paulson@16061
   137
       in
paulson@16061
   138
	   mksubstlist rest newlist
paulson@16061
   139
       end;
quigley@15642
   140
quigley@15642
   141
(* based on Tactic.distinct_subgoals_tac *)
quigley@15642
   142
quigley@15642
   143
fun delete_assump_tac state lit =
quigley@15642
   144
    let val (frozth,thawfn) = freeze_thaw state
quigley@15642
   145
        val froz_prems = cprems_of frozth
quigley@15642
   146
        val assumed = implies_elim_list frozth (map assume froz_prems)
paulson@16061
   147
        val new_prems = ReconOrderClauses.remove_nth lit froz_prems
quigley@15642
   148
        val implied = implies_intr_list new_prems assumed
quigley@15642
   149
    in  
quigley@15642
   150
        Seq.single (thawfn implied)  
quigley@15642
   151
    end
quigley@15642
   152
quigley@15642
   153
quigley@15642
   154
quigley@15642
   155
quigley@15642
   156
quigley@15642
   157
(*************************************)
quigley@15642
   158
(* Reconstruct a factoring step      *)
quigley@15642
   159
(*************************************)
quigley@15642
   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 
paulson@16061
   164
      val th =  valOf (assoc (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 
paulson@16061
   232
      val th1 =  valOf (assoc (thml,clause1))
paulson@16061
   233
      val th2 =  valOf (assoc (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
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
quigley@15642
   256
                          let 
paulson@15774
   257
                            val th1 =  valOf (assoc (thml,clause1))
paulson@15774
   258
                            val th2 =  valOf (assoc (thml,clause2)) 
quigley@15642
   259
                            val eq_lit_th = select_literal (lit1+1) th1
quigley@15642
   260
                            val mod_lit_th = select_literal (lit2+1) th2
quigley@15642
   261
                            val eqsubst = eq_lit_th RSN (2,rev_subst)
quigley@15642
   262
                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
quigley@15642
   263
			    val newth' =negate_nead newth 
quigley@15642
   264
                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars)
quigley@15642
   265
                            val thmvars = thm_vars res
quigley@15642
   266
                         in 
quigley@15642
   267
                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
quigley@15642
   268
                         end
paulson@15774
   269
			 handle Option => reconstruction_failed "follow_standard_para"
quigley@15642
   270
quigley@15642
   271
*)
quigley@15642
   272
quigley@15642
   273
quigley@15642
   274
(********************************)
quigley@15642
   275
(* Reconstruct a rewriting step *)
quigley@15642
   276
(********************************)
quigley@15642
   277
 
quigley@15642
   278
(*
quigley@15642
   279
quigley@15642
   280
val rev_subst = rotate_prems 1 subst;
quigley@15642
   281
quigley@15642
   282
fun paramod_rule ((cl1, lit1), (cl2 , lit2)) =
quigley@15642
   283
     let  val eq_lit_th = select_literal (lit1+1) cl1
quigley@15642
   284
          val mod_lit_th = select_literal (lit2+1) cl2
quigley@15642
   285
          val eqsubst = eq_lit_th RSN (2,rev_subst)
quigley@15642
   286
          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
quigley@15642
   287
eqsubst)
paulson@15697
   288
     in Meson.negated_asm_of_head newth end;
quigley@15642
   289
quigley@15642
   290
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
quigley@15642
   291
eqsubst)
quigley@15642
   292
quigley@15642
   293
val mod_lit_th' = mod_lit_th RS not_sym
quigley@15642
   294
quigley@15642
   295
*)
quigley@15642
   296
quigley@15642
   297
quigley@15642
   298
fun delete_assumps 0 th = th 
quigley@15642
   299
|   delete_assumps n th = let val th_prems = length (prems_of th)
quigley@15642
   300
                              val th' = hd (Seq.list_of(delete_assump_tac  th (th_prems -1)))
quigley@15642
   301
                          in
quigley@15642
   302
                              delete_assumps (n-1) th'
quigley@15642
   303
                          end
quigley@15642
   304
quigley@15642
   305
(* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
quigley@15642
   306
(* changed negate_nead to negate_head here too*)
quigley@15642
   307
                    (* clause1, lit1 is thing to rewrite with *)
quigley@16548
   308
(*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = 
paulson@16061
   309
      let val th1 =  valOf (assoc (thml,clause1))
paulson@16061
   310
	  val th2 = valOf (assoc (thml,clause2))
paulson@16061
   311
	  val eq_lit_th = select_literal (lit1+1) th1
paulson@16061
   312
	  val mod_lit_th = select_literal (lit2+1) th2
paulson@16061
   313
	  val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@16061
   314
	  val eq_lit_prem_num = length (prems_of eq_lit_th)
wenzelm@16433
   315
	  val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2)
paulson@16061
   316
	  val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
paulson@16061
   317
     	  val newthm = negate_head newth
paulson@16061
   318
	  val newthm' = delete_assumps eq_lit_prem_num newthm
paulson@16061
   319
	  val (res, numlist, symlist, nsymlist) =
paulson@16061
   320
	      ReconOrderClauses.rearrange_clause newthm clause_strs allvars
paulson@16061
   321
	  val thmvars = thm_vars res
paulson@16061
   322
       in
paulson@16061
   323
	   (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
paulson@16061
   324
       end
paulson@16061
   325
       handle Option => reconstruction_failed "follow_rewrite"
quigley@15642
   326
quigley@16548
   327
*)
quigley@15642
   328
quigley@15642
   329
(*****************************************)
quigley@15642
   330
(* Reconstruct an obvious reduction step *)
quigley@15642
   331
(*****************************************)
quigley@15642
   332
quigley@15642
   333
paulson@16061
   334
fun follow_obvious  (clause1, lit1)  allvars thml clause_strs = 
paulson@16061
   335
    let val th1 =  valOf (assoc (thml,clause1))
paulson@16061
   336
	val prems1 = prems_of th1
paulson@16061
   337
	val newthm = refl RSN ((lit1+ 1), th1)
paulson@16061
   338
		     handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
paulson@16061
   339
	val (res, numlist, symlist, nsymlist) =
paulson@16061
   340
	    ReconOrderClauses.rearrange_clause newthm clause_strs allvars
paulson@16061
   341
	val thmvars = thm_vars res
paulson@16061
   342
    in 
paulson@16061
   343
	(res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
paulson@16061
   344
    end
paulson@16061
   345
    handle Option => reconstruction_failed "follow_obvious"
quigley@15642
   346
quigley@15642
   347
(**************************************************************************************)
quigley@15642
   348
(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
quigley@15642
   349
(**************************************************************************************)
quigley@15642
   350
quigley@15642
   351
 fun follow_proof clauses allvars  clausenum thml  (Axiom ) clause_strs
quigley@15642
   352
        = follow_axiom clauses allvars  clausenum thml clause_strs
quigley@15642
   353
quigley@15642
   354
      | follow_proof clauses  allvars clausenum  thml (Binary (a, b)) clause_strs
quigley@15642
   355
        = follow_binary  (a, b)  allvars thml clause_strs
quigley@15642
   356
quigley@15642
   357
      | follow_proof clauses  allvars clausenum  thml (MRR (a, b)) clause_strs
quigley@15642
   358
        = follow_mrr (a, b)  allvars thml clause_strs
quigley@15642
   359
quigley@15642
   360
      | follow_proof clauses  allvars clausenum  thml (Factor (a, b, c)) clause_strs
quigley@15642
   361
         = follow_factor a b c  allvars thml clause_strs
quigley@15642
   362
quigley@15642
   363
      | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
quigley@15642
   364
        = follow_standard_para (a, b) allvars  thml clause_strs
quigley@15642
   365
quigley@16548
   366
    (*  | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
quigley@16548
   367
        = follow_rewrite (a,b)  allvars thml clause_strs*)
quigley@15642
   368
quigley@15642
   369
      | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
quigley@15642
   370
        = follow_obvious (a,b)  allvars thml clause_strs
quigley@15642
   371
quigley@15642
   372
      (*| follow_proof clauses  clausenum thml (Hyper l)
quigley@15642
   373
        = follow_hyper l thml*)
quigley@15642
   374
      | follow_proof clauses  allvars clausenum  thml _ _ =
quigley@15642
   375
          raise ASSERTION  "proof step not implemented"
quigley@15642
   376
quigley@15642
   377
quigley@15642
   378
quigley@15642
   379
 
quigley@15642
   380
(**************************************************************************************)
quigley@15642
   381
(* reconstruct a single line of the res. proof - at the moment do only inference steps*)
quigley@15642
   382
(**************************************************************************************)
quigley@15642
   383
quigley@15642
   384
    fun follow_line clauses  allvars thml (clause_num, proof_step, clause_strs) recons
quigley@15642
   385
        = let
quigley@15642
   386
            val (thm, recon_fun) = follow_proof clauses  allvars clause_num thml proof_step clause_strs 
quigley@15642
   387
            val recon_step = (recon_fun)
quigley@15642
   388
          in
quigley@15642
   389
            (((clause_num, thm)::thml), ((clause_num,recon_step)::recons))
quigley@15642
   390
          end
quigley@15642
   391
quigley@15642
   392
(***************************************************************)
quigley@15642
   393
(* follow through the res. proof, creating an Isabelle theorem *)
quigley@15642
   394
(***************************************************************)
quigley@15642
   395
quigley@15642
   396
quigley@15642
   397
quigley@15642
   398
(*fun is_proof_char ch = (case ch of 
quigley@15642
   399
                       
quigley@15642
   400
                        "(" => true
quigley@15642
   401
                       |  ")" => true
quigley@15642
   402
                         | ":" => true
quigley@15642
   403
                        |  "'" => true
quigley@15642
   404
                        |  "&" => true
quigley@15642
   405
                        | "|" => true
quigley@15642
   406
                        | "~" => true
quigley@15642
   407
                        |  "." => true
quigley@15642
   408
                        |(is_alpha ) => true
quigley@15642
   409
                       |(is_digit) => true
quigley@15642
   410
                         | _ => false)*)
quigley@15642
   411
quigley@15642
   412
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
quigley@15642
   413
quigley@15642
   414
fun proofstring x = let val exp = explode x 
quigley@15642
   415
                    in
quigley@15642
   416
                        List.filter (is_proof_char ) exp
quigley@15642
   417
                    end
quigley@15642
   418
quigley@15642
   419
quigley@15642
   420
fun not_newline ch = not (ch = "\n");
quigley@15642
   421
quigley@15642
   422
(*
quigley@15642
   423
quigley@15642
   424
fun follow clauses [] allvars thml recons = 
quigley@15642
   425
                             let (* val _ = reset show_sorts*)
paulson@15736
   426
                              val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml))
quigley@15642
   427
                              val thmproofstring = proofstring ( thmstring)
quigley@15642
   428
                            val no_returns =List.filter  not_newline ( thmproofstring)
quigley@15642
   429
                            val thmstr = implode no_returns
wenzelm@16259
   430
                               val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file")))
quigley@15642
   431
                               val _ = TextIO.output(outfile, "thmstr is "^thmstr)
quigley@15642
   432
                               val _ = TextIO.flushOut outfile;
quigley@15642
   433
                               val _ =  TextIO.closeOut outfile
quigley@15642
   434
                                 (*val _ = set show_sorts*)
quigley@15642
   435
                             in
quigley@15642
   436
                                  ((snd( hd thml)), recons)
quigley@15642
   437
                             end
quigley@15642
   438
      | follow clauses (h::t) allvars thml recons 
quigley@15642
   439
        = let
quigley@15642
   440
            val (thml', recons') = follow_line clauses allvars  thml h recons
quigley@15642
   441
            val  (thm, recons_list) = follow clauses t  allvars thml' recons'
quigley@15642
   442
            
quigley@15642
   443
quigley@15642
   444
          in
quigley@15642
   445
             (thm,recons_list)
quigley@15642
   446
          end
quigley@15642
   447
quigley@15642
   448
*)
quigley@15642
   449
paulson@16061
   450
fun replace_clause_strs [] recons newrecons = (newrecons)
paulson@16061
   451
|   replace_clause_strs ((thmnum, thm)::thml)    
paulson@16061
   452
                  ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
paulson@16061
   453
    let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm
paulson@16061
   454
    in
paulson@16061
   455
	replace_clause_strs thml recons  
paulson@16061
   456
	    ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
paulson@16061
   457
    end
quigley@15642
   458
quigley@15642
   459
quigley@15642
   460
fun follow clauses [] allvars thml recons = 
paulson@16061
   461
      let 
paulson@16061
   462
	  val new_recons = replace_clause_strs thml recons []
paulson@16061
   463
      in
paulson@16061
   464
	   (#2(hd thml), new_recons)
paulson@16061
   465
      end
paulson@16061
   466
 | follow clauses (h::t) allvars thml recons =
paulson@16061
   467
      let
paulson@16061
   468
	val (thml', recons') = follow_line clauses allvars  thml h recons
paulson@16061
   469
	val  (thm, recons_list) = follow clauses t  allvars thml' recons'     
paulson@16061
   470
      in
paulson@16061
   471
	 (thm,recons_list)
paulson@16061
   472
      end
quigley@15642
   473
quigley@15642
   474
quigley@15642
   475
quigley@15642
   476
(* Assume we have the cnf clauses as a list of (clauseno, clause) *)
quigley@15642
   477
 (* and the proof as a list of the proper datatype *)
quigley@15642
   478
(* take the cnf clauses of the goal and the proof from the res. prover *)
quigley@15642
   479
(* as a list of type Proofstep and return the thm goal ==> False *)
quigley@15642
   480
quigley@15642
   481
fun first_pair (a,b,c) = (a,b);
quigley@15642
   482
quigley@15642
   483
fun second_pair (a,b,c) = (b,c);
quigley@15642
   484
quigley@15642
   485
(* takes original axioms, proof_steps parsed from spass, variables *)
quigley@15642
   486
quigley@15642
   487
fun translate_proof clauses proof allvars
quigley@15642
   488
        = let val (thm, recons) = follow clauses proof allvars [] []
quigley@15642
   489
          in
quigley@15642
   490
             (thm, (recons))
quigley@15642
   491
          end
quigley@15642
   492
  
quigley@15642
   493
quigley@15642
   494
quigley@15642
   495
fun remove_tinfo [] = []
paulson@16061
   496
  | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) =
paulson@16061
   497
      (clausenum, step , newstrs)::(remove_tinfo xs)