# HG changeset patch # User mengj # Date 1145331398 -7200 # Node ID ad8bb8346e511675a8e24d664a4194cd7f832823 # Parent a479b800cc8c71ab56009f9bbf245c51d4e970ea Tidied up some programs. diff -r a479b800cc8c -r ad8bb8346e51 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Sun Apr 16 08:22:29 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Tue Apr 18 05:36:38 2006 +0200 @@ -313,18 +313,6 @@ end | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); -fun logic_of_nclauses [] (lg,seen) = (lg,seen) - | logic_of_nclauses (cls::clss) (FOL,seen) = - logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen)) - | logic_of_nclauses clss (lg,seen) = (lg,seen); - -fun problem_logic (goal_cls,rules_cls) = - let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[]) - val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1) - in - lg2 - end; - fun problem_logic_goals_aux [] (lg,seen) = lg | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen)); @@ -360,13 +348,13 @@ fun write_subgoal_file mode ctxt conjectures user_thms n = - let val conj_cls = map prop_of (make_clauses conjectures) - val hyp_cls = map prop_of (cnf_hyps_thms ctxt) + let val conj_cls = make_clauses conjectures + val hyp_cls = cnf_hyps_thms ctxt val goal_cls = conj_cls@hyp_cls val user_rules = map ResAxioms.pairname user_thms - 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) + 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) val thy = ProofContext.theory_of ctxt - val prob_logic = case mode of Auto => problem_logic_goals [goal_cls] + val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls] | Fol => FOL | Hol => HOL val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol () @@ -465,7 +453,7 @@ fun write_problem_files pf (ctxt,th) = let val goals = Thm.prems_of th val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) - 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 *) + 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 *) val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ Int.toString (Array.length names_arr)) val thy = ProofContext.theory_of ctxt @@ -475,12 +463,12 @@ let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th) val negs = Option.valOf (metahyps_thms n st) - val negs_clauses = map prop_of (make_clauses negs) + val negs_clauses = make_clauses negs in negs_clauses::(get_neg_subgoals (n - 1)) end val neg_subgoals = get_neg_subgoals (length goals) - val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals neg_subgoals + val goals_logic = case !linkup_logic_mode of Auto => problem_logic_goals (map (map prop_of) neg_subgoals) | Fol => FOL | Hol => HOL val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol () @@ -491,7 +479,7 @@ val writer = (*if !prover ~= "spass" then *)tptp_writer fun write_all [] _ = [] | write_all (subgoal::subgoals) k = - (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1)) + (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1)) in (write_all neg_subgoals (length goals), names_arr) end; diff -r a479b800cc8c -r ad8bb8346e51 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Sun Apr 16 08:22:29 2006 +0200 +++ b/src/HOL/Tools/res_axioms.ML Tue Apr 18 05:36:38 2006 +0200 @@ -12,22 +12,15 @@ val elimRule_tac : thm -> Tactical.tactic val elimR2Fol : thm -> term val transform_elim : thm -> thm - val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list - val clausify_axiom_pairsH : (string*thm) -> (ResHolClause.clause*thm) list val cnf_axiom : (string * thm) -> thm list val meta_cnf_axiom : thm -> thm list val claset_rules_of_thy : theory -> (string * thm) list val simpset_rules_of_thy : theory -> (string * thm) list val claset_rules_of_ctxt: Proof.context -> (string * thm) list val simpset_rules_of_ctxt : Proof.context -> (string * thm) list - val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list - val clausify_rules_pairsH : (string*thm) list -> (ResHolClause.clause*thm) list list val pairname : thm -> (string * thm) val skolem_thm : thm -> thm list - val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list - val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list; - val clausify_rules_pairs_abs : (string * thm) list -> (Term.term * (string * int)) list list val meson_method_setup : theory -> theory val setup : theory -> theory @@ -391,19 +384,6 @@ (*works for both FOL and HOL*) val cnf_rules = cnf_rules_g cnf_axiom; -fun cnf_rules1 [] err_list = ([],err_list) - | cnf_rules1 ((name,th) :: ths) err_list = - let val (ts,es) = cnf_rules1 ths err_list - in ((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end; - -fun cnf_rules2 [] err_list = ([],err_list) - | cnf_rules2 ((name,th) :: ths) err_list = - let val (ts,es) = cnf_rules2 ths err_list - in - ((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) - end; - - fun cnf_rules_pairs_aux [] = [] | cnf_rules_pairs_aux ((name,th)::ths) = let val ts = cnf_rules_pairs_aux ths @@ -418,70 +398,9 @@ fun cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms); -fun clausify_rules_pairs_abs_aux [] = [] - | clausify_rules_pairs_abs_aux ((name,th)::ths) = - let val ts = clausify_rules_pairs_abs_aux ths - fun pair_name_cls k (n, []) = [] - | pair_name_cls k (n, cls::clss) = - (prop_of cls, (n,k)) :: (pair_name_cls (k+1) (n, clss)) - in - pair_name_cls 0 (name, (cnf_axiom(name,th))) :: ts - handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts - end; - -fun clausify_rules_pairs_abs thms = rev (clausify_rules_pairs_abs_aux thms); - (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) -fun make_axiom_clauses _ _ [] = [] - | make_axiom_clauses name i (th::ths) = - case ResClause.make_axiom_clause (prop_of th) (name,i) of - SOME cls => (cls, th) :: make_axiom_clauses name (i+1) ths - | NONE => make_axiom_clauses name i ths; - -(* outputs a list of (clause,theorem) pairs *) -fun clausify_axiom_pairs (name,th) = - filter (fn (c,th) => not (ResClause.isTaut c)) - (make_axiom_clauses name 0 (cnf_axiom (name,th))); - -fun make_axiom_clausesH _ _ [] = [] - | make_axiom_clausesH name i (th::ths) = - (ResHolClause.make_axiom_clause (prop_of th) (name,i), th) :: - (make_axiom_clausesH name (i+1) ths) - -fun clausify_axiom_pairsH (name,th) = - filter (fn (c,th) => not (ResHolClause.isTaut c)) - (make_axiom_clausesH name 0 (cnf_axiom (name,th))); - - -fun clausify_rules_pairs_aux result [] = result - | clausify_rules_pairs_aux result ((name,th)::ths) = - clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths - handle THM (msg,_,_) => - (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); - clausify_rules_pairs_aux result ths) - | ResClause.CLAUSE (msg,t) => - (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg ^ - ": " ^ TermLib.string_of_term t); - clausify_rules_pairs_aux result ths) - - -fun clausify_rules_pairs_auxH result [] = result - | clausify_rules_pairs_auxH result ((name,th)::ths) = - clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths - handle THM (msg,_,_) => - (Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); - clausify_rules_pairs_auxH result ths) - | ResHolClause.LAM2COMB (t) => - (Output.debug ("Cannot clausify " ^ TermLib.string_of_term t); - clausify_rules_pairs_auxH result ths) - - - -val clausify_rules_pairs = clausify_rules_pairs_aux []; - -val clausify_rules_pairsH = clausify_rules_pairs_auxH []; (*These should include any plausibly-useful theorems, especially if they need Skolem functions. FIXME: this list is VERY INCOMPLETE*)