src/HOL/Tools/ATP/recon_translate_proof.ML
changeset 15774 9df37a0e935d
parent 15739 bb2acfed8212
child 15789 4cb16144c81b
     1.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue Apr 19 15:15:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue Apr 19 18:08:44 2005 +0200
     1.3 @@ -62,18 +62,20 @@
     1.4                                   implode(List.filter is_alpha_space_digit_or_neg exp_term)
     1.5                               end
     1.6  
     1.7 +fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
     1.8  
     1.9  (****************************************)
    1.10  (* Reconstruct an axiom resolution step *)
    1.11  (****************************************)
    1.12  
    1.13 - fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
    1.14 -                                     let val this_axiom =(Recon_Base.assoc  clausenum clauses)
    1.15 +fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
    1.16 +                                     let val this_axiom = valOf (assoc (clauses,clausenum))
    1.17                                           val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)         
    1.18                                           val thmvars = thm_vars res
    1.19                                       in
    1.20                                           (res, (Axiom,clause_strs,thmvars )  )
    1.21                                       end
    1.22 +                                     handle Option => reconstruction_failed "follow_axiom"
    1.23  
    1.24  (****************************************)
    1.25  (* Reconstruct a binary resolution step *)
    1.26 @@ -82,14 +84,15 @@
    1.27                   (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
    1.28  fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs 
    1.29          = let
    1.30 -              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
    1.31 -              val thm2 =  Recon_Base.assoc  clause2 thml
    1.32 +              val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    1.33 +              val thm2 =  valOf (assoc (thml,clause2))
    1.34                val res =   thm1 RSN ((lit2 +1), thm2)
    1.35                val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    1.36                val thmvars = thm_vars res
    1.37            in
    1.38               (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
    1.39            end
    1.40 +	  handle Option => reconstruction_failed "follow_binary"
    1.41  
    1.42  
    1.43  
    1.44 @@ -100,14 +103,15 @@
    1.45  
    1.46  fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs 
    1.47          = let
    1.48 -              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
    1.49 -              val thm2 =  Recon_Base.assoc  clause2 thml
    1.50 +              val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    1.51 +              val thm2 =  valOf (assoc (thml,clause2))
    1.52                val res =   thm1 RSN ((lit2 +1), thm2)
    1.53                val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    1.54                val thmvars = thm_vars res
    1.55            in
    1.56               (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
    1.57            end
    1.58 +	  handle Option => reconstruction_failed "follow_mrr"
    1.59  
    1.60  
    1.61  (*******************************************)
    1.62 @@ -144,7 +148,7 @@
    1.63  (*FIXME: share code with that in Tools/reconstruction.ML*)
    1.64  fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
    1.65                            let 
    1.66 -                            val th =  Recon_Base.assoc clause thml
    1.67 +                            val th =  valOf (assoc (thml,clause))
    1.68                              val prems = prems_of th
    1.69                              val sign = sign_of_thm th
    1.70                              val fac1 = get_nth (lit1+1) prems
    1.71 @@ -178,15 +182,8 @@
    1.72                                  in 
    1.73                                         (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
    1.74                                  end
    1.75 -                         end;
    1.76 -
    1.77 -
    1.78 -
    1.79 -Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False";
    1.80 -val prems = it;
    1.81 -br (hd prems) 1;
    1.82 -br (hd(tl(tl prems))) 1;
    1.83 -qed "merge";
    1.84 +                         end
    1.85 +                         handle Option => reconstruction_failed "follow_factor"
    1.86  
    1.87  
    1.88  
    1.89 @@ -217,8 +214,8 @@
    1.90  
    1.91  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
    1.92                            let 
    1.93 -                            val th1 =  Recon_Base.assoc clause1 thml
    1.94 -                            val th2 =  Recon_Base.assoc clause2 thml 
    1.95 +                            val th1 =  valOf (assoc (thml,clause1))
    1.96 +                            val th2 =  valOf (assoc (thml,clause2)) 
    1.97                              val eq_lit_th = select_literal (lit1+1) th1
    1.98                              val mod_lit_th = select_literal (lit2+1) th2
    1.99                              val eqsubst = eq_lit_th RSN (2,rev_subst)
   1.100 @@ -236,12 +233,13 @@
   1.101                           in 
   1.102                             (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
   1.103                           end
   1.104 +			 handle Option => reconstruction_failed "follow_standard_para"
   1.105  
   1.106  (*              
   1.107  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
   1.108                            let 
   1.109 -                            val th1 =  Recon_Base.assoc clause1 thml
   1.110 -                            val th2 =  Recon_Base.assoc clause2 thml 
   1.111 +                            val th1 =  valOf (assoc (thml,clause1))
   1.112 +                            val th2 =  valOf (assoc (thml,clause2)) 
   1.113                              val eq_lit_th = select_literal (lit1+1) th1
   1.114                              val mod_lit_th = select_literal (lit2+1) th2
   1.115                              val eqsubst = eq_lit_th RSN (2,rev_subst)
   1.116 @@ -252,6 +250,7 @@
   1.117                           in 
   1.118                             (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
   1.119                           end
   1.120 +			 handle Option => reconstruction_failed "follow_standard_para"
   1.121  
   1.122  *)
   1.123  
   1.124 @@ -292,8 +291,8 @@
   1.125                      (* clause1, lit1 is thing to rewrite with *)
   1.126  fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= 
   1.127  
   1.128 -                          let val th1 =  Recon_Base.assoc clause1 thml
   1.129 -                              val th2 = Recon_Base.assoc clause2 thml
   1.130 +                          let val th1 =  valOf (assoc (thml,clause1))
   1.131 +                              val th2 = valOf (assoc (thml,clause2))
   1.132                                val eq_lit_th = select_literal (lit1+1) th1
   1.133                                val mod_lit_th = select_literal (lit2+1) th2
   1.134                                val eqsubst = eq_lit_th RSN (2,rev_subst)
   1.135 @@ -309,6 +308,7 @@
   1.136                             in
   1.137                                 (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
   1.138                             end
   1.139 +			   handle Option => reconstruction_failed "follow_rewrite"
   1.140  
   1.141  
   1.142  
   1.143 @@ -318,7 +318,7 @@
   1.144  
   1.145  
   1.146  fun follow_obvious  (clause1, lit1)  allvars thml clause_strs= 
   1.147 -                           let val th1 =  Recon_Base.assoc clause1 thml
   1.148 +                           let val th1 =  valOf (assoc (thml,clause1))
   1.149                                 val prems1 = prems_of th1
   1.150                                 val newthm = refl RSN ((lit1+ 1), th1)
   1.151                                                 handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
   1.152 @@ -327,6 +327,7 @@
   1.153                             in 
   1.154                                 (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
   1.155                             end
   1.156 +  	 		   handle Option => reconstruction_failed "follow_obvious"
   1.157  
   1.158  (**************************************************************************************)
   1.159  (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)