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