src/HOL/Tools/res_atp.ML
changeset 19442 ad8bb8346e51
parent 19352 1a07f6cf1e6c
child 19445 da75577642a9
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sun Apr 16 08:22:29 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Apr 18 05:36:38 2006 +0200
     1.3 @@ -313,18 +313,6 @@
     1.4      end
     1.5    | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
     1.6  
     1.7 -fun logic_of_nclauses [] (lg,seen) = (lg,seen)
     1.8 -  | logic_of_nclauses (cls::clss) (FOL,seen) =
     1.9 -    logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
    1.10 -  | logic_of_nclauses clss (lg,seen) = (lg,seen);
    1.11 -
    1.12 -fun problem_logic (goal_cls,rules_cls) =
    1.13 -    let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[])
    1.14 -	val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1)
    1.15 -    in
    1.16 -	lg2
    1.17 -    end;
    1.18 -
    1.19  fun problem_logic_goals_aux [] (lg,seen) = lg
    1.20    | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
    1.21      problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
    1.22 @@ -360,13 +348,13 @@
    1.23  
    1.24  
    1.25  fun write_subgoal_file mode ctxt conjectures user_thms n =
    1.26 -    let val conj_cls = map prop_of (make_clauses conjectures) 
    1.27 -	val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
    1.28 +    let val conj_cls = make_clauses conjectures 
    1.29 +	val hyp_cls = cnf_hyps_thms ctxt
    1.30  	val goal_cls = conj_cls@hyp_cls
    1.31  	val user_rules = map ResAxioms.pairname user_thms
    1.32 -	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
    1.33 +	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (map prop_of goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
    1.34  	val thy = ProofContext.theory_of ctxt
    1.35 -	val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
    1.36 +	val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
    1.37  				    | Fol => FOL
    1.38  				    | Hol => HOL
    1.39  	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
    1.40 @@ -465,7 +453,7 @@
    1.41  fun write_problem_files pf (ctxt,th)  =
    1.42    let val goals = Thm.prems_of th
    1.43        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
    1.44 -      val (names_arr, axclauses_as_terms) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
    1.45 +      val (names_arr, axclauses) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
    1.46        val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
    1.47                       Int.toString (Array.length names_arr))
    1.48        val thy = ProofContext.theory_of ctxt
    1.49 @@ -475,12 +463,12 @@
    1.50  	      let val st = Seq.hd (EVERY'
    1.51  				       [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th)
    1.52  		  val negs = Option.valOf (metahyps_thms n st)
    1.53 -		  val negs_clauses = map prop_of (make_clauses negs)
    1.54 +		  val negs_clauses = make_clauses negs
    1.55  	      in
    1.56  		  negs_clauses::(get_neg_subgoals (n - 1))
    1.57  	      end
    1.58        val neg_subgoals = get_neg_subgoals (length goals) 
    1.59 -      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals neg_subgoals
    1.60 +      val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals (map (map prop_of) neg_subgoals)
    1.61  						 | Fol => FOL
    1.62  						 | Hol => HOL
    1.63        val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
    1.64 @@ -491,7 +479,7 @@
    1.65        val writer = (*if !prover ~= "spass" then *)tptp_writer 
    1.66        fun write_all [] _ = []
    1.67  	| write_all (subgoal::subgoals) k =
    1.68 -	  (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
    1.69 +	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
    1.70    in
    1.71        (write_all neg_subgoals (length goals), names_arr)
    1.72    end;