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