src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 15774 9df37a0e935d
parent 15739 bb2acfed8212
child 15782 a1863ea9052b
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 19 15:15:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 19 18:08:44 2005 +0200
     1.3 @@ -116,7 +116,9 @@
     1.4  fun get_step_nums [] nums = nums
     1.5  |   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
     1.6  
     1.7 -fun assoc_snd a [] = raise Recon_Base.Noassoc
     1.8 +exception Noassoc;
     1.9 +
    1.10 +fun assoc_snd a [] = raise Noassoc
    1.11    | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
    1.12  
    1.13  (* change to be something using check_order  instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
    1.14 @@ -125,13 +127,10 @@
    1.15  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
    1.16  *)
    1.17  (*FIX - should this have vars in it? *)
    1.18 -fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))                        
    1.19 -                               in 
    1.20 -                                   true
    1.21 -                              end
    1.22 -                              handle EXCEP => false
    1.23 +fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true) 
    1.24 +                               handle _ => false
    1.25  
    1.26 -fun assoc_out_of_order a [] = raise Recon_Base.Noassoc
    1.27 +fun assoc_out_of_order a [] = raise Noassoc
    1.28  |   assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
    1.29  
    1.30  fun get_assoc_snds [] xs assocs= assocs
    1.31 @@ -180,7 +179,7 @@
    1.32                                              (* literals of -all- axioms, not just those used by spass *)
    1.33                                              val meta_strs = map get_meta_lits metas
    1.34                                             
    1.35 -                                            val metas_and_strs = zip  metas meta_strs
    1.36 +                                            val metas_and_strs = ListPair.zip (metas,meta_strs)
    1.37                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    1.38                                               val _ = TextIO.output (outfile, onestr ax_strs)
    1.39                                               
    1.40 @@ -193,14 +192,14 @@
    1.41  
    1.42                                              val ax_metas = get_assoc_snds ax_strs metas_and_strs []
    1.43                                              val ax_vars = map thm_vars ax_metas
    1.44 -                                            val ax_with_vars = zip ax_metas ax_vars
    1.45 +                                            val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
    1.46  
    1.47                                              (* get list of extra axioms as thms with their variables *)
    1.48                                              val extra_metas = add_if_not_inlist metas ax_metas []
    1.49                                              val extra_vars = map thm_vars extra_metas
    1.50                                              val extra_with_vars = if (not (extra_metas = []) ) 
    1.51                                                                    then
    1.52 - 									 zip extra_metas extra_vars
    1.53 + 									 ListPair.zip (extra_metas,extra_vars)
    1.54                                                                    else
    1.55                                                                           []
    1.56  
    1.57 @@ -218,7 +217,7 @@
    1.58                                             val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
    1.59                                             
    1.60                                           in
    1.61 -                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (zip step_nums ax_metas))
    1.62 +                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
    1.63                                           end
    1.64                                          
    1.65  fun thmstrings [] str = str
    1.66 @@ -347,12 +346,12 @@
    1.67                                                    (* do the bit for the Isabelle ordered axioms at the top *)
    1.68                                                    val ax_nums = map #1 numcls
    1.69                                                    val ax_strs = map get_meta_lits_bracket (map #2 numcls)
    1.70 -                                                  val numcls_strs = zip ax_nums ax_strs
    1.71 +                                                  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
    1.72                                                    val num_cls_vars =  map (addvars vars) numcls_strs;
    1.73 -                                                  val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
    1.74 +                                                  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
    1.75                                                    
    1.76                                                    val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
    1.77 -                                                  val reconExtraAxStr = extraAxs_to_string ( zip extra_nums extra_with_vars) ""
    1.78 +                                                  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
    1.79                                                    val frees_str = "["^(thmvars_to_string frees "")^"]"
    1.80                                                    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
    1.81  
    1.82 @@ -640,15 +639,15 @@
    1.83  
    1.84  fun to_isar_proof (frees, xs, goalstring) = let val extraaxioms = get_extraaxioms xs
    1.85                             val extraax_num = length extraaxioms
    1.86 -                           val origaxioms_and_steps = drop (extraax_num) xs  
    1.87 +                           val origaxioms_and_steps = Library.drop (extraax_num, xs)  
    1.88                            
    1.89    
    1.90                             val origaxioms = get_origaxioms origaxioms_and_steps
    1.91                             val origax_num = length origaxioms
    1.92 -                           val axioms_and_steps = drop (origax_num + extraax_num) xs  
    1.93 +                           val axioms_and_steps = Library.drop (origax_num + extraax_num, xs)  
    1.94                             val axioms = get_axioms axioms_and_steps
    1.95                             
    1.96 -                           val steps = drop origax_num axioms_and_steps
    1.97 +                           val steps = Library.drop (origax_num, axioms_and_steps)
    1.98                             val firststeps = butlast steps
    1.99                             val laststep = last steps
   1.100                             val goalstring = implode(butlast(explode goalstring))