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.
2 fun take n [] = []
3 |   take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs)))
5 fun drop n [] = []
6 |   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
8 fun remove n [] = []
9 |   remove n (x::xs) = List.filter (not_equal n) (x::xs);
11 fun remove_nth n [] = []
12 |   remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs))
14 fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
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
22 fun add_once x [] = [x]
23 |   add_once x (y::ys) = if (inlist x (y::ys)) then
24                             (y::ys)
25                         else
28 fun thm_vars thm = map getindexstring (map fst (Drule.vars_of thm));
30 Goal "False ==> False";
31 by Auto_tac;
32 qed "False_imp";
34 exception Reflex_equal;
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]  *)
41 datatype Side = Left |Right
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
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
64 datatype Step_label = T_info
65                      |P_info
68 fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ")
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
79 (****************************************)
80 (* Reconstruct an axiom resolution step *)
81 (****************************************)
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
91 (****************************************)
92 (* Reconstruct a binary resolution step *)
93 (****************************************)
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
109 (******************************************************)
110 (* Reconstruct a matching replacement resolution step *)
111 (******************************************************)
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
126 (*******************************************)
127 (* Reconstruct a factoring resolution step *)
128 (*******************************************)
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;
137 (* based on Tactic.distinct_subgoals_tac *)
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
153 (*************************************)
154 (* Reconstruct a factoring step      *)
155 (*************************************)
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
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;
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";
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
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
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
232 (*************************************)
233 (* Reconstruct a paramodulation step *)
234 (*************************************)
236 val rev_subst = rotate_prems 1 subst;
237 val rev_ssubst = rotate_prems 1 ssubst;
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)
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)
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
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)
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
279 *)
282 (********************************)
283 (* Reconstruct a rewriting step *)
284 (********************************)
286 (*
288 val rev_subst = rotate_prems 1 subst;
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)
298 val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1
299 eqsubst)
301 val mod_lit_th' = mod_lit_th RS not_sym
303 *)
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
313 (* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
315                     (* clause1, lit1 is thing to rewrite with *)
316 fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs=
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)
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
338 (*****************************************)
339 (* Reconstruct an obvious reduction step *)
340 (*****************************************)
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
354 (**************************************************************************************)
355 (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
356 (**************************************************************************************)
358  fun follow_proof clauses allvars  clausenum thml  (Axiom ) clause_strs
359         = follow_axiom clauses allvars  clausenum thml clause_strs
361       | follow_proof clauses  allvars clausenum  thml (Binary (a, b)) clause_strs
362         = follow_binary  (a, b)  allvars thml clause_strs
364       | follow_proof clauses  allvars clausenum  thml (MRR (a, b)) clause_strs
365         = follow_mrr (a, b)  allvars thml clause_strs
367       | follow_proof clauses  allvars clausenum  thml (Factor (a, b, c)) clause_strs
368          = follow_factor a b c  allvars thml clause_strs
370       | follow_proof clauses  allvars clausenum  thml (Para (a, b)) clause_strs
371         = follow_standard_para (a, b) allvars  thml clause_strs
373       | follow_proof clauses  allvars clausenum thml (Rewrite (a,b)) clause_strs
374         = follow_rewrite (a,b)  allvars thml clause_strs
376       | follow_proof clauses  allvars clausenum thml (Obvious (a,b)) clause_strs
377         = follow_obvious (a,b)  allvars thml clause_strs
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"
387 (**************************************************************************************)
388 (* reconstruct a single line of the res. proof - at the moment do only inference steps*)
389 (**************************************************************************************)
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
399 (***************************************************************)
400 (* follow through the res. proof, creating an Isabelle theorem *)
401 (***************************************************************)
405 (*fun is_proof_char ch = (case ch of
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)*)
419 fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ")
421 fun proofstring x = let val exp = explode x
422                     in
423                         List.filter (is_proof_char ) exp
424                     end
427 fun not_newline ch = not (ch = "\n");
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 (*
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'
454           in
455              (thm,recons_list)
456           end
458 *)
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
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
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
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 *)
490 fun first_pair (a,b,c) = (a,b);
492 fun second_pair (a,b,c) = (b,c);
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;
499 (* takes original axioms, proof_steps parsed from spass, variables *)
501 fun translate_proof clauses proof allvars
502         = let val (thm, recons) = follow clauses proof allvars [] []
503           in
504              (thm, (recons))
505           end
509 fun remove_tinfo [] = []
510 |   remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs)