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